Step | Hyp | Ref
| Expression |
1 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜
∅)) |
2 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜
∅)) |
3 | 2 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜
∅))) |
4 | 1, 3 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = ∅ → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 ∅) = (𝐴 +𝑜 (𝐵 +𝑜
∅)))) |
5 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
6 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝑦)) |
7 | 6 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
8 | 5, 7 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
9 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦)) |
10 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 suc 𝑦)) |
11 | 10 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))) |
12 | 9, 11 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))) |
13 | | oveq2 6658 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ((𝐴 +𝑜 𝐵) +𝑜 𝐶)) |
14 | | oveq2 6658 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 +𝑜 𝑥) = (𝐵 +𝑜 𝐶)) |
15 | 14 | oveq2d 6666 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))) |
16 | 13, 15 | eqeq12d 2637 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) ↔ ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))) |
17 | | oacl 7615 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 𝐵) ∈ On) |
18 | | oa0 7596 |
. . . . . 6
⊢ ((𝐴 +𝑜 𝐵) ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 ∅)
= (𝐴 +𝑜
𝐵)) |
19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅)
= (𝐴 +𝑜
𝐵)) |
20 | | oa0 7596 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 +𝑜 ∅)
= 𝐵) |
21 | 20 | oveq2d 6666 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 +𝑜 (𝐵 +𝑜 ∅))
= (𝐴 +𝑜
𝐵)) |
22 | 21 | adantl 482 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 ∅))
= (𝐴 +𝑜
𝐵)) |
23 | 19, 22 | eqtr4d 2659 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 ∅)
= (𝐴 +𝑜
(𝐵 +𝑜
∅))) |
24 | | suceq 5790 |
. . . . . 6
⊢ (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
25 | | oasuc 7604 |
. . . . . . . 8
⊢ (((𝐴 +𝑜 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc
𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
26 | 17, 25 | sylan 488 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 suc
𝑦) = suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
27 | | oasuc 7604 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 suc 𝑦) = suc (𝐵 +𝑜 𝑦)) |
28 | 27 | oveq2d 6666 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦))) |
29 | 28 | adantl 482 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = (𝐴 +𝑜 suc (𝐵 +𝑜 𝑦))) |
30 | | oacl 7615 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +𝑜 𝑦) ∈ On) |
31 | | oasuc 7604 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On) → (𝐴 +𝑜 suc
(𝐵 +𝑜
𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
32 | 30, 31 | sylan2 491 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 suc
(𝐵 +𝑜
𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
33 | 29, 32 | eqtrd 2656 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
34 | 33 | anassrs 680 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
35 | 26, 34 | eqeq12d 2637 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 suc
𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)) ↔ suc ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = suc (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
36 | 24, 35 | syl5ibr 236 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦)))) |
37 | 36 | expcom 451 |
. . . 4
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 suc 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 suc 𝑦))))) |
38 | | vex 3203 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
39 | | oalim 7612 |
. . . . . . . . . 10
⊢ (((𝐴 +𝑜 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
40 | 38, 39 | mpanr1 719 |
. . . . . . . . 9
⊢ (((𝐴 +𝑜 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
41 | 17, 40 | sylan 488 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
42 | 41 | ancoms 469 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
43 | 42 | adantr 481 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
44 | | oalimcl 7640 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +𝑜 𝑥)) |
45 | 38, 44 | mpanr1 719 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +𝑜 𝑥)) |
46 | 45 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → Lim (𝐵 +𝑜 𝑥)) |
47 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝐵 +𝑜 𝑥) ∈ V |
48 | | oalim 7612 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ ((𝐵 +𝑜 𝑥) ∈ V ∧ Lim (𝐵 +𝑜 𝑥))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
49 | 47, 48 | mpanr1 719 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ Lim (𝐵 +𝑜 𝑥)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
50 | 46, 49 | sylan2 491 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
51 | | limelon 5788 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
52 | 38, 51 | mpan 706 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
53 | | oacl 7615 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On) |
54 | 53 | ancoms 469 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +𝑜 𝑥) ∈ On) |
55 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐵 +𝑜 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On) |
56 | 55 | ex 450 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 +𝑜 𝑥) ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On)) |
57 | 54, 56 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → 𝑧 ∈ On)) |
58 | 57 | adantld 483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)) |
59 | 58 | adantl 482 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ∈ On)) |
60 | | 0ellim 5787 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
61 | | onelss 5766 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐵 ∈ On → (𝑧 ∈ 𝐵 → 𝑧 ⊆ 𝐵)) |
62 | 20 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝐵 ∈ On → (𝑧 ⊆ (𝐵 +𝑜 ∅) ↔ 𝑧 ⊆ 𝐵)) |
63 | 61, 62 | sylibrd 249 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 ∈ On → (𝑧 ∈ 𝐵 → 𝑧 ⊆ (𝐵 +𝑜
∅))) |
64 | 63 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ 𝐵) → 𝑧 ⊆ (𝐵 +𝑜
∅)) |
65 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (𝑦 = ∅ → (𝐵 +𝑜 𝑦) = (𝐵 +𝑜
∅)) |
66 | 65 | sseq2d 3633 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ 𝑧 ⊆ (𝐵 +𝑜
∅))) |
67 | 66 | rspcev 3309 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ ((∅
∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +𝑜 ∅)) →
∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
68 | 60, 64, 67 | syl2an 494 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Lim
𝑥 ∧ (𝐵 ∈ On ∧ 𝑧 ∈ 𝐵)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
69 | 68 | expr 643 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
70 | 69 | adantrl 752 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
71 | 70 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
72 | | oawordex 7637 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧)) |
73 | 72 | ad2ant2l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵 ⊆ 𝑧 ↔ ∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧)) |
74 | | oaord 7627 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥))) |
75 | 74 | 3expb 1266 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦 ∈ 𝑥 ↔ (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥))) |
76 | | eleq1 2689 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐵 +𝑜 𝑦) = 𝑧 → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥))) |
77 | 75, 76 | sylan9bb 736 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ (((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥))) |
78 | 77 | an32s 846 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +𝑜 𝑥))) |
79 | 78 | biimpar 502 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑦 ∈ 𝑥) |
80 | | eqimss2 3658 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐵 +𝑜 𝑦) = 𝑧 → 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
81 | 80 | ad3antlr 767 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
82 | 79, 81 | jca 554 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
83 | 82 | anasss 679 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥))) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
84 | 83 | expcom 451 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ((𝑦 ∈ On ∧ (𝐵 +𝑜 𝑦) = 𝑧) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +𝑜 𝑦)))) |
85 | 84 | reximdv2 3014 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
86 | 85 | adantrr 753 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ On (𝐵 +𝑜 𝑦) = 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
87 | 73, 86 | sylbid 230 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝐵 ⊆ 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
88 | 87 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝐵 ⊆ 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))) |
89 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝑧 ∈ On → Ord 𝑧) |
90 | | eloni 5733 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (𝐵 ∈ On → Ord 𝐵) |
91 | | ordtri2or 5822 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((Ord
𝑧 ∧ Ord 𝐵) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
92 | 89, 90, 91 | syl2anr 495 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
93 | 92 | ad2ant2l 782 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On)) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
94 | 93 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
95 | 71, 88, 94 | mpjaod 396 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +𝑜 𝑥) ∧ 𝑧 ∈ On))) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
96 | 95 | exp45 642 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (Lim
𝑥 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦))))) |
97 | 96 | imp 445 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))) |
98 | 97 | adantld 483 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)))) |
99 | 98 | imp32 449 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦)) |
100 | | simplrr 801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ On) |
101 | | onelon 5748 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
102 | 101, 30 | sylan2 491 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ 𝑥)) → (𝐵 +𝑜 𝑦) ∈ On) |
103 | 102 | exp32 631 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐵 ∈ On → (𝑥 ∈ On → (𝑦 ∈ 𝑥 → (𝐵 +𝑜 𝑦) ∈ On))) |
104 | 103 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑥 ∈ On → (𝐵 ∈ On → (𝑦 ∈ 𝑥 → (𝐵 +𝑜 𝑦) ∈ On))) |
105 | 104 | imp31 448 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝑥) → (𝐵 +𝑜 𝑦) ∈ On) |
106 | 105 | adantll 750 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑦 ∈ 𝑥) → (𝐵 +𝑜 𝑦) ∈ On) |
107 | 106 | adantlr 751 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → (𝐵 +𝑜 𝑦) ∈ On) |
108 | | simpll 790 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On) → 𝐴 ∈ On) |
109 | 108 | ad2antlr 763 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) |
110 | | oaword 7629 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑧 ∈ On ∧ (𝐵 +𝑜 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
111 | 100, 107,
109, 110 | syl3anc 1326 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
112 | 111 | rexbidva 3049 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +𝑜 𝑦) ↔ ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
113 | 99, 112 | mpbid 222 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
114 | 113 | exp32 631 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))) |
115 | 59, 114 | mpdd 43 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
116 | 115 | exp32 631 |
. . . . . . . . . . . . . . . . 17
⊢ (Lim
𝑥 → (𝑥 ∈ On → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))) |
117 | 52, 116 | mpd 15 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +𝑜 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))) |
118 | 117 | exp4a 633 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝑥 → (𝐵 ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))))) |
119 | 118 | imp31 448 |
. . . . . . . . . . . . . 14
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 +𝑜 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
120 | 119 | ralrimiv 2965 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 +𝑜 𝑥)∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
121 | | iunss2 4565 |
. . . . . . . . . . . . 13
⊢
(∀𝑧 ∈
(𝐵 +𝑜
𝑥)∃𝑦 ∈ 𝑥 (𝐴 +𝑜 𝑧) ⊆ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∪
𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
122 | 120, 121 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
123 | 122 | ancoms 469 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
124 | | oaordi 7626 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 → (𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥))) |
125 | 124 | anim1d 588 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝑥 ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))))) |
126 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 +𝑜 𝑦) → (𝐴 +𝑜 𝑧) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
127 | 126 | eleq2d 2687 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐵 +𝑜 𝑦) → (𝑤 ∈ (𝐴 +𝑜 𝑧) ↔ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)))) |
128 | 127 | rspcev 3309 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 +𝑜 𝑦) ∈ (𝐵 +𝑜 𝑥) ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)) |
129 | 125, 128 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝑥 ∧ 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))) |
130 | 129 | expd 452 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 → (𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)))) |
131 | 130 | rexlimdv 3030 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (∃𝑦 ∈ 𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧))) |
132 | | eliun 4524 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑤 ∈ (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
133 | | eliun 4524 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) ↔ ∃𝑧 ∈ (𝐵 +𝑜 𝑥)𝑤 ∈ (𝐴 +𝑜 𝑧)) |
134 | 131, 132,
133 | 3imtr4g 285 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑤 ∈ ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → 𝑤 ∈ ∪
𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧))) |
135 | 134 | ssrdv 3609 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
136 | 52, 135 | sylan 488 |
. . . . . . . . . . . 12
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
137 | 136 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧)) |
138 | 123, 137 | eqssd 3620 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑧 ∈ (𝐵 +𝑜 𝑥)(𝐴 +𝑜 𝑧) = ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
139 | 50, 138 | eqtrd 2656 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
140 | 139 | an12s 843 |
. . . . . . . 8
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
141 | 140 | adantr 481 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
142 | | iuneq2 4537 |
. . . . . . . 8
⊢
(∀𝑦 ∈
𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ∪
𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
143 | 142 | adantl 482 |
. . . . . . 7
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ∪ 𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) |
144 | 141, 143 | eqtr4d 2659 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → (𝐴 +𝑜 (𝐵 +𝑜 𝑥)) = ∪
𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦)) |
145 | 43, 144 | eqtr4d 2659 |
. . . . 5
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦))) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥))) |
146 | 145 | exp31 630 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 ((𝐴 +𝑜 𝐵) +𝑜 𝑦) = (𝐴 +𝑜 (𝐵 +𝑜 𝑦)) → ((𝐴 +𝑜 𝐵) +𝑜 𝑥) = (𝐴 +𝑜 (𝐵 +𝑜 𝑥))))) |
147 | 4, 8, 12, 16, 23, 37, 146 | tfinds3 7064 |
. . 3
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))) |
148 | 147 | com12 32 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶)))) |
149 | 148 | 3impia 1261 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +𝑜 𝐵) +𝑜 𝐶) = (𝐴 +𝑜 (𝐵 +𝑜 𝐶))) |