Step | Hyp | Ref
| Expression |
1 | | unfilem1.2 |
. . . . . . . . . 10
⊢ 𝐵 ∈ ω |
2 | | elnn 7075 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ 𝐵 ∧ 𝐵 ∈ ω) → 𝑥 ∈ ω) |
3 | 1, 2 | mpan2 707 |
. . . . . . . . 9
⊢ (𝑥 ∈ 𝐵 → 𝑥 ∈ ω) |
4 | | unfilem1.1 |
. . . . . . . . . 10
⊢ 𝐴 ∈ ω |
5 | | nnaord 7699 |
. . . . . . . . . 10
⊢ ((𝑥 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐴 ∈ ω) → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵))) |
6 | 1, 4, 5 | mp3an23 1416 |
. . . . . . . . 9
⊢ (𝑥 ∈ ω → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵))) |
7 | 3, 6 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ 𝐵 → (𝑥 ∈ 𝐵 ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵))) |
8 | 7 | ibi 256 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵)) |
9 | | nnaword1 7709 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → 𝐴 ⊆ (𝐴 +𝑜 𝑥)) |
10 | | nnord 7073 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ ω → Ord 𝐴) |
11 | 4, 10 | ax-mp 5 |
. . . . . . . . . 10
⊢ Ord 𝐴 |
12 | | nnacl 7691 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 +𝑜 𝑥) ∈
ω) |
13 | | nnord 7073 |
. . . . . . . . . . 11
⊢ ((𝐴 +𝑜 𝑥) ∈ ω → Ord
(𝐴 +𝑜
𝑥)) |
14 | 12, 13 | syl 17 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → Ord
(𝐴 +𝑜
𝑥)) |
15 | | ordtri1 5756 |
. . . . . . . . . 10
⊢ ((Ord
𝐴 ∧ Ord (𝐴 +𝑜 𝑥)) → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)) |
16 | 11, 14, 15 | sylancr 695 |
. . . . . . . . 9
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → (𝐴 ⊆ (𝐴 +𝑜 𝑥) ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)) |
17 | 9, 16 | mpbid 222 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑥 ∈ ω) → ¬
(𝐴 +𝑜
𝑥) ∈ 𝐴) |
18 | 4, 3, 17 | sylancr 695 |
. . . . . . 7
⊢ (𝑥 ∈ 𝐵 → ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴) |
19 | 8, 18 | jca 554 |
. . . . . 6
⊢ (𝑥 ∈ 𝐵 → ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)) |
20 | | eleq1 2689 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ↔ (𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵))) |
21 | | eleq1 2689 |
. . . . . . . . 9
⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ 𝐴 ↔ (𝐴 +𝑜 𝑥) ∈ 𝐴)) |
22 | 21 | notbid 308 |
. . . . . . . 8
⊢ (𝑦 = (𝐴 +𝑜 𝑥) → (¬ 𝑦 ∈ 𝐴 ↔ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴)) |
23 | 20, 22 | anbi12d 747 |
. . . . . . 7
⊢ (𝑦 = (𝐴 +𝑜 𝑥) → ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) ↔ ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴))) |
24 | 23 | biimparc 504 |
. . . . . 6
⊢ ((((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ∧ ¬ (𝐴 +𝑜 𝑥) ∈ 𝐴) ∧ 𝑦 = (𝐴 +𝑜 𝑥)) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
25 | 19, 24 | sylan 488 |
. . . . 5
⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 = (𝐴 +𝑜 𝑥)) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
26 | 25 | rexlimiva 3028 |
. . . 4
⊢
(∃𝑥 ∈
𝐵 𝑦 = (𝐴 +𝑜 𝑥) → (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
27 | 4, 1 | nnacli 7694 |
. . . . . . . 8
⊢ (𝐴 +𝑜 𝐵) ∈
ω |
28 | | elnn 7075 |
. . . . . . . 8
⊢ ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ (𝐴 +𝑜 𝐵) ∈ ω) → 𝑦 ∈ ω) |
29 | 27, 28 | mpan2 707 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → 𝑦 ∈ ω) |
30 | | nnord 7073 |
. . . . . . . . 9
⊢ (𝑦 ∈ ω → Ord 𝑦) |
31 | | ordtri1 5756 |
. . . . . . . . 9
⊢ ((Ord
𝐴 ∧ Ord 𝑦) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴)) |
32 | 10, 30, 31 | syl2an 494 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ⊆ 𝑦 ↔ ¬ 𝑦 ∈ 𝐴)) |
33 | | nnawordex 7717 |
. . . . . . . 8
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (𝐴 ⊆ 𝑦 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦)) |
34 | 32, 33 | bitr3d 270 |
. . . . . . 7
⊢ ((𝐴 ∈ ω ∧ 𝑦 ∈ ω) → (¬
𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦)) |
35 | 4, 29, 34 | sylancr 695 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (¬ 𝑦 ∈ 𝐴 ↔ ∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦)) |
36 | | eleq1 2689 |
. . . . . . . . . 10
⊢ ((𝐴 +𝑜 𝑥) = 𝑦 → ((𝐴 +𝑜 𝑥) ∈ (𝐴 +𝑜 𝐵) ↔ 𝑦 ∈ (𝐴 +𝑜 𝐵))) |
37 | 6, 36 | sylan9bb 736 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → (𝑥 ∈ 𝐵 ↔ 𝑦 ∈ (𝐴 +𝑜 𝐵))) |
38 | 37 | biimprcd 240 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑥 ∈ 𝐵)) |
39 | | eqcom 2629 |
. . . . . . . . . . 11
⊢ ((𝐴 +𝑜 𝑥) = 𝑦 ↔ 𝑦 = (𝐴 +𝑜 𝑥)) |
40 | 39 | biimpi 206 |
. . . . . . . . . 10
⊢ ((𝐴 +𝑜 𝑥) = 𝑦 → 𝑦 = (𝐴 +𝑜 𝑥)) |
41 | 40 | adantl 482 |
. . . . . . . . 9
⊢ ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑦 = (𝐴 +𝑜 𝑥)) |
42 | 41 | a1i 11 |
. . . . . . . 8
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → 𝑦 = (𝐴 +𝑜 𝑥))) |
43 | 38, 42 | jcad 555 |
. . . . . . 7
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → ((𝑥 ∈ ω ∧ (𝐴 +𝑜 𝑥) = 𝑦) → (𝑥 ∈ 𝐵 ∧ 𝑦 = (𝐴 +𝑜 𝑥)))) |
44 | 43 | reximdv2 3014 |
. . . . . 6
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (∃𝑥 ∈ ω (𝐴 +𝑜 𝑥) = 𝑦 → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥))) |
45 | 35, 44 | sylbid 230 |
. . . . 5
⊢ (𝑦 ∈ (𝐴 +𝑜 𝐵) → (¬ 𝑦 ∈ 𝐴 → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥))) |
46 | 45 | imp 445 |
. . . 4
⊢ ((𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴) → ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥)) |
47 | 26, 46 | impbii 199 |
. . 3
⊢
(∃𝑥 ∈
𝐵 𝑦 = (𝐴 +𝑜 𝑥) ↔ (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
48 | | unfilem1.3 |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝐵 ↦ (𝐴 +𝑜 𝑥)) |
49 | | ovex 6678 |
. . . 4
⊢ (𝐴 +𝑜 𝑥) ∈ V |
50 | 48, 49 | elrnmpti 5376 |
. . 3
⊢ (𝑦 ∈ ran 𝐹 ↔ ∃𝑥 ∈ 𝐵 𝑦 = (𝐴 +𝑜 𝑥)) |
51 | | eldif 3584 |
. . 3
⊢ (𝑦 ∈ ((𝐴 +𝑜 𝐵) ∖ 𝐴) ↔ (𝑦 ∈ (𝐴 +𝑜 𝐵) ∧ ¬ 𝑦 ∈ 𝐴)) |
52 | 47, 50, 51 | 3bitr4i 292 |
. 2
⊢ (𝑦 ∈ ran 𝐹 ↔ 𝑦 ∈ ((𝐴 +𝑜 𝐵) ∖ 𝐴)) |
53 | 52 | eqriv 2619 |
1
⊢ ran 𝐹 = ((𝐴 +𝑜 𝐵) ∖ 𝐴) |