| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o ∅)) |
| 2 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 +o 𝑥) = (𝐵 +o ∅)) |
| 3 | 2 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o ∅))) |
| 4 | 1, 3 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = ∅ → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o (𝐵 +o
∅)))) |
| 5 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o 𝑦)) |
| 6 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o 𝑦)) |
| 7 | 6 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o 𝑦))) |
| 8 | 5, 7 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)))) |
| 9 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o suc 𝑦)) |
| 10 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o suc 𝑦)) |
| 11 | 10 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o suc 𝑦))) |
| 12 | 9, 11 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = suc 𝑦 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦)))) |
| 13 | | oveq2 7439 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 +o 𝐵) +o 𝑥) = ((𝐴 +o 𝐵) +o 𝐶)) |
| 14 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 +o 𝑥) = (𝐵 +o 𝐶)) |
| 15 | 14 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐴 +o (𝐵 +o 𝑥)) = (𝐴 +o (𝐵 +o 𝐶))) |
| 16 | 13, 15 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐶 → (((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥)) ↔ ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))) |
| 17 | | oacl 8573 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o 𝐵) ∈ On) |
| 18 | | oa0 8554 |
. . . . . 6
⊢ ((𝐴 +o 𝐵) ∈ On → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o 𝐵)) |
| 19 | 17, 18 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o 𝐵)) |
| 20 | | oa0 8554 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 +o ∅) = 𝐵) |
| 21 | 20 | oveq2d 7447 |
. . . . . 6
⊢ (𝐵 ∈ On → (𝐴 +o (𝐵 +o ∅)) =
(𝐴 +o 𝐵)) |
| 22 | 21 | adantl 481 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o (𝐵 +o ∅)) =
(𝐴 +o 𝐵)) |
| 23 | 19, 22 | eqtr4d 2780 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o ∅) = (𝐴 +o (𝐵 +o
∅))) |
| 24 | | suceq 6450 |
. . . . . 6
⊢ (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → suc ((𝐴 +o 𝐵) +o 𝑦) = suc (𝐴 +o (𝐵 +o 𝑦))) |
| 25 | | oasuc 8562 |
. . . . . . . 8
⊢ (((𝐴 +o 𝐵) ∈ On ∧ 𝑦 ∈ On) → ((𝐴 +o 𝐵) +o suc 𝑦) = suc ((𝐴 +o 𝐵) +o 𝑦)) |
| 26 | 17, 25 | sylan 580 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → ((𝐴 +o 𝐵) +o suc 𝑦) = suc ((𝐴 +o 𝐵) +o 𝑦)) |
| 27 | | oasuc 8562 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦)) |
| 28 | 27 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 +o (𝐵 +o suc 𝑦)) = (𝐴 +o suc (𝐵 +o 𝑦))) |
| 29 | 28 | adantl 481 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o (𝐵 +o suc 𝑦)) = (𝐴 +o suc (𝐵 +o 𝑦))) |
| 30 | | oacl 8573 |
. . . . . . . . . 10
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o 𝑦) ∈ On) |
| 31 | | oasuc 8562 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (𝐵 +o 𝑦) ∈ On) → (𝐴 +o suc (𝐵 +o 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦))) |
| 32 | 30, 31 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o suc (𝐵 +o 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦))) |
| 33 | 29, 32 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 +o (𝐵 +o suc 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦))) |
| 34 | 33 | anassrs 467 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (𝐴 +o (𝐵 +o suc 𝑦)) = suc (𝐴 +o (𝐵 +o 𝑦))) |
| 35 | 26, 34 | eqeq12d 2753 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦)) ↔ suc ((𝐴 +o 𝐵) +o 𝑦) = suc (𝐴 +o (𝐵 +o 𝑦)))) |
| 36 | 24, 35 | imbitrrid 246 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ On) → (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦)))) |
| 37 | 36 | expcom 413 |
. . . 4
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o suc 𝑦) = (𝐴 +o (𝐵 +o suc 𝑦))))) |
| 38 | | iuneq2 5011 |
. . . . . . 7
⊢
(∀𝑦 ∈
𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ∪
𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 39 | 38 | adantl 481 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 40 | | vex 3484 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
| 41 | | oalim 8570 |
. . . . . . . . . 10
⊢ (((𝐴 +o 𝐵) ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → ((𝐴 +o 𝐵) +o 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦)) |
| 42 | 40, 41 | mpanr1 703 |
. . . . . . . . 9
⊢ (((𝐴 +o 𝐵) ∈ On ∧ Lim 𝑥) → ((𝐴 +o 𝐵) +o 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦)) |
| 43 | 17, 42 | sylan 580 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ Lim 𝑥) → ((𝐴 +o 𝐵) +o 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦)) |
| 44 | 43 | ancoms 458 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 +o 𝐵) +o 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦)) |
| 45 | 44 | adantr 480 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → ((𝐴 +o 𝐵) +o 𝑥) = ∪ 𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦)) |
| 46 | | oalimcl 8598 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +o 𝑥)) |
| 47 | 40, 46 | mpanr1 703 |
. . . . . . . . . . 11
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +o 𝑥)) |
| 48 | 47 | ancoms 458 |
. . . . . . . . . 10
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → Lim (𝐵 +o 𝑥)) |
| 49 | | ovex 7464 |
. . . . . . . . . . 11
⊢ (𝐵 +o 𝑥) ∈ V |
| 50 | | oalim 8570 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ ((𝐵 +o 𝑥) ∈ V ∧ Lim (𝐵 +o 𝑥))) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 51 | 49, 50 | mpanr1 703 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 52 | 48, 51 | sylan2 593 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 53 | | limelon 6448 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
| 54 | 40, 53 | mpan 690 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
| 55 | | oacl 8573 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +o 𝑥) ∈ On) |
| 56 | 55 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑥) ∈ On) |
| 57 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 +o 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On) |
| 58 | 57 | ex 412 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 +o 𝑥) ∈ On → (𝑧 ∈ (𝐵 +o 𝑥) → 𝑧 ∈ On)) |
| 59 | 56, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → 𝑧 ∈ On)) |
| 60 | 59 | adantld 490 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On)) |
| 61 | 60 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On)) |
| 62 | | 0ellim 6447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
| 63 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 ∈ On → (𝑧 ∈ 𝐵 → 𝑧 ⊆ 𝐵)) |
| 64 | 20 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝐵 ∈ On → (𝑧 ⊆ (𝐵 +o ∅) ↔ 𝑧 ⊆ 𝐵)) |
| 65 | 63, 64 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝐵 ∈ On → (𝑧 ∈ 𝐵 → 𝑧 ⊆ (𝐵 +o ∅))) |
| 66 | 65 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ 𝐵) → 𝑧 ⊆ (𝐵 +o ∅)) |
| 67 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (𝑦 = ∅ → (𝐵 +o 𝑦) = (𝐵 +o ∅)) |
| 68 | 67 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (𝑦 = ∅ → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ 𝑧 ⊆ (𝐵 +o ∅))) |
| 69 | 68 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((∅
∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +o ∅)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 70 | 62, 66, 69 | syl2an 596 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Lim
𝑥 ∧ (𝐵 ∈ On ∧ 𝑧 ∈ 𝐵)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 71 | 70 | expr 456 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 72 | 71 | adantrl 716 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 73 | 72 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝑧 ∈ 𝐵 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 74 | | oawordex 8595 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧)) |
| 75 | 74 | ad2ant2l 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝐵 ⊆ 𝑧 ↔ ∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧)) |
| 76 | | oaord 8585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝑦 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 ↔ (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥))) |
| 77 | 76 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦 ∈ 𝑥 ↔ (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥))) |
| 78 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐵 +o 𝑦) = 𝑧 → ((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ↔ 𝑧 ∈ (𝐵 +o 𝑥))) |
| 79 | 77, 78 | sylan9bb 509 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ (((𝑦 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑦) = 𝑧) → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +o 𝑥))) |
| 80 | 79 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑦 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +o 𝑥))) |
| 81 | 80 | biimpar 477 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑦 ∈ 𝑥) |
| 82 | | eqimss2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐵 +o 𝑦) = 𝑧 → 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 83 | 82 | ad3antlr 731 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 84 | 81, 83 | jca 511 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ ((((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 85 | 84 | anasss 466 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥))) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 86 | 85 | expcom 413 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ((𝑦 ∈ On ∧ (𝐵 +o 𝑦) = 𝑧) → (𝑦 ∈ 𝑥 ∧ 𝑧 ⊆ (𝐵 +o 𝑦)))) |
| 87 | 86 | reximdv2 3164 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 88 | 87 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ On (𝐵 +o 𝑦) = 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 89 | 75, 88 | sylbid 240 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝐵 ⊆ 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 90 | 89 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝐵 ⊆ 𝑧 → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))) |
| 91 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑧 ∈ On → Ord 𝑧) |
| 92 | | eloni 6394 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐵 ∈ On → Ord 𝐵) |
| 93 | | ordtri2or 6482 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((Ord
𝑧 ∧ Ord 𝐵) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
| 94 | 91, 92, 93 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
| 95 | 94 | ad2ant2l 746 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On)) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
| 96 | 95 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → (𝑧 ∈ 𝐵 ∨ 𝐵 ⊆ 𝑧)) |
| 97 | 73, 90, 96 | mpjaod 861 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Lim
𝑥 ∧ ((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ (𝑧 ∈ (𝐵 +o 𝑥) ∧ 𝑧 ∈ On))) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 98 | 97 | exp45 438 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
𝑥 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦))))) |
| 99 | 98 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))) |
| 100 | 99 | adantld 490 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)))) |
| 101 | 100 | imp32 418 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦)) |
| 102 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → 𝑧 ∈ On) |
| 103 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑥 ∈ On ∧ 𝑦 ∈ 𝑥) → 𝑦 ∈ On) |
| 104 | 103, 30 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ On ∧ 𝑦 ∈ 𝑥)) → (𝐵 +o 𝑦) ∈ On) |
| 105 | 104 | exp32 420 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝐵 ∈ On → (𝑥 ∈ On → (𝑦 ∈ 𝑥 → (𝐵 +o 𝑦) ∈ On))) |
| 106 | 105 | com12 32 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ On → (𝐵 ∈ On → (𝑦 ∈ 𝑥 → (𝐵 +o 𝑦) ∈ On))) |
| 107 | 106 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ 𝑥) → (𝐵 +o 𝑦) ∈ On) |
| 108 | 107 | ad4ant24 754 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → (𝐵 +o 𝑦) ∈ On) |
| 109 | | simpll 767 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On) → 𝐴 ∈ On) |
| 110 | 109 | ad2antlr 727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → 𝐴 ∈ On) |
| 111 | | oaword 8587 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑧 ∈ On ∧ (𝐵 +o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))) |
| 112 | 102, 108,
110, 111 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) ∧ 𝑦 ∈ 𝑥) → (𝑧 ⊆ (𝐵 +o 𝑦) ↔ (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))) |
| 113 | 112 | rexbidva 3177 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → (∃𝑦 ∈ 𝑥 𝑧 ⊆ (𝐵 +o 𝑦) ↔ ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))) |
| 114 | 101, 113 | mpbid 232 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) ∧ 𝑧 ∈ On)) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))) |
| 115 | 114 | exp32 420 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ On → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))) |
| 116 | 61, 115 | mpdd 43 |
. . . . . . . . . . . . . . . . 17
⊢ ((Lim
𝑥 ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))) |
| 117 | 116 | exp32 420 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → (𝑥 ∈ On → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))))) |
| 118 | 54, 117 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ (Lim
𝑥 → (𝐵 ∈ On → ((𝐴 ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))))) |
| 119 | 118 | exp4a 431 |
. . . . . . . . . . . . . 14
⊢ (Lim
𝑥 → (𝐵 ∈ On → (𝐴 ∈ On → (𝑧 ∈ (𝐵 +o 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))))) |
| 120 | 119 | imp31 417 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → ∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)))) |
| 121 | 120 | ralrimiv 3145 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦))) |
| 122 | | iunss2 5049 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(𝐵 +o 𝑥)∃𝑦 ∈ 𝑥 (𝐴 +o 𝑧) ⊆ (𝐴 +o (𝐵 +o 𝑦)) → ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 123 | 121, 122 | syl 17 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝐴 ∈ On) → ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 124 | 123 | ancoms 458 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ⊆ ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 125 | | oaordi 8584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 → (𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥))) |
| 126 | 125 | anim1d 611 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝑥 ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))))) |
| 127 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐵 +o 𝑦) → (𝐴 +o 𝑧) = (𝐴 +o (𝐵 +o 𝑦))) |
| 128 | 127 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝐵 +o 𝑦) → (𝑤 ∈ (𝐴 +o 𝑧) ↔ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)))) |
| 129 | 128 | rspcev 3622 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐵 +o 𝑦) ∈ (𝐵 +o 𝑥) ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧)) |
| 130 | 126, 129 | syl6 35 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ((𝑦 ∈ 𝑥 ∧ 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧))) |
| 131 | 130 | expd 415 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑦 ∈ 𝑥 → (𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧)))) |
| 132 | 131 | rexlimdv 3153 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (∃𝑦 ∈ 𝑥 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦)) → ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧))) |
| 133 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦)) ↔ ∃𝑦 ∈ 𝑥 𝑤 ∈ (𝐴 +o (𝐵 +o 𝑦))) |
| 134 | | eliun 4995 |
. . . . . . . . . . . . . 14
⊢ (𝑤 ∈ ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) ↔ ∃𝑧 ∈ (𝐵 +o 𝑥)𝑤 ∈ (𝐴 +o 𝑧)) |
| 135 | 132, 133,
134 | 3imtr4g 296 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑤 ∈ ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦)) → 𝑤 ∈ ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧))) |
| 136 | 135 | ssrdv 3989 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 137 | 54, 136 | sylan 580 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 138 | 137 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦)) ⊆ ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧)) |
| 139 | 124, 138 | eqssd 4001 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 +o 𝑧) = ∪ 𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 140 | 52, 139 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 141 | 140 | an12s 649 |
. . . . . . 7
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 142 | 141 | adantr 480 |
. . . . . 6
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → (𝐴 +o (𝐵 +o 𝑥)) = ∪
𝑦 ∈ 𝑥 (𝐴 +o (𝐵 +o 𝑦))) |
| 143 | 39, 45, 142 | 3eqtr4d 2787 |
. . . . 5
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦))) → ((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥))) |
| 144 | 143 | exp31 419 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 ((𝐴 +o 𝐵) +o 𝑦) = (𝐴 +o (𝐵 +o 𝑦)) → ((𝐴 +o 𝐵) +o 𝑥) = (𝐴 +o (𝐵 +o 𝑥))))) |
| 145 | 4, 8, 12, 16, 23, 37, 144 | tfinds3 7886 |
. . 3
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))) |
| 146 | 145 | com12 32 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐶 ∈ On → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶)))) |
| 147 | 146 | 3impia 1118 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → ((𝐴 +o 𝐵) +o 𝐶) = (𝐴 +o (𝐵 +o 𝐶))) |