| Step | Hyp | Ref
| Expression |
| 1 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐵 +o 𝑥) = (𝐵 +o ∅)) |
| 2 | 1 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = ∅ → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o ∅))) |
| 3 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) |
| 4 | 3 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o
∅))) |
| 5 | 2, 4 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = ∅ → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o ∅)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o
∅)))) |
| 6 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o 𝑦)) |
| 7 | 6 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o 𝑦))) |
| 8 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) |
| 9 | 8 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) |
| 10 | 7, 9 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝑦 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) |
| 11 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐵 +o 𝑥) = (𝐵 +o suc 𝑦)) |
| 12 | 11 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o suc 𝑦))) |
| 13 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) |
| 14 | 13 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))) |
| 15 | 12, 14 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))) |
| 16 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐵 +o 𝑥) = (𝐵 +o 𝐶)) |
| 17 | 16 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝐶 → (𝐴 ·o (𝐵 +o 𝑥)) = (𝐴 ·o (𝐵 +o 𝐶))) |
| 18 | | oveq2 7439 |
. . . . . 6
⊢ (𝑥 = 𝐶 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝐶)) |
| 19 | 18 | oveq2d 7447 |
. . . . 5
⊢ (𝑥 = 𝐶 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) |
| 20 | 17, 19 | eqeq12d 2753 |
. . . 4
⊢ (𝑥 = 𝐶 → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))) |
| 21 | | omcl 8574 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o 𝐵) ∈ On) |
| 22 | | oa0 8554 |
. . . . . 6
⊢ ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝐵) +o ∅) =
(𝐴 ·o
𝐵)) |
| 23 | 21, 22 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) +o ∅) =
(𝐴 ·o
𝐵)) |
| 24 | | om0 8555 |
. . . . . . 7
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
| 25 | 24 | adantr 480 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o ∅) =
∅) |
| 26 | 25 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o ∅))
= ((𝐴 ·o
𝐵) +o
∅)) |
| 27 | | oa0 8554 |
. . . . . . 7
⊢ (𝐵 ∈ On → (𝐵 +o ∅) = 𝐵) |
| 28 | 27 | adantl 481 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o ∅) = 𝐵) |
| 29 | 28 | oveq2d 7447 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o ∅)) =
(𝐴 ·o
𝐵)) |
| 30 | 23, 26, 29 | 3eqtr4rd 2788 |
. . . 4
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o ∅)) =
((𝐴 ·o
𝐵) +o (𝐴 ·o
∅))) |
| 31 | | oveq1 7438 |
. . . . . . . 8
⊢ ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴)) |
| 32 | | oasuc 8562 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦)) |
| 33 | 32 | 3adant1 1131 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o suc 𝑦) = suc (𝐵 +o 𝑦)) |
| 34 | 33 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o (𝐵 +o suc 𝑦)) = (𝐴 ·o suc (𝐵 +o 𝑦))) |
| 35 | | oacl 8573 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐵 +o 𝑦) ∈ On) |
| 36 | | omsuc 8564 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ (𝐵 +o 𝑦) ∈ On) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴)) |
| 37 | 35, 36 | sylan2 593 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ (𝐵 ∈ On ∧ 𝑦 ∈ On)) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴)) |
| 38 | 37 | 3impb 1115 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc (𝐵 +o 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴)) |
| 39 | 34, 38 | eqtrd 2777 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴)) |
| 40 | | omsuc 8564 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
| 41 | 40 | 3adant2 1132 |
. . . . . . . . . . 11
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o suc 𝑦) = ((𝐴 ·o 𝑦) +o 𝐴)) |
| 42 | 41 | oveq2d 7447 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))) |
| 43 | | omcl 8574 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑦) ∈ On) |
| 44 | | oaass 8599 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐴 ·o 𝐵) ∈ On ∧ (𝐴 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))) |
| 45 | 21, 44 | syl3an1 1164 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ·o 𝑦) ∈ On ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))) |
| 46 | 43, 45 | syl3an2 1165 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 ∈ On ∧ 𝑦 ∈ On) ∧ 𝐴 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))) |
| 47 | 46 | 3exp 1120 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))))) |
| 48 | 47 | exp4b 430 |
. . . . . . . . . . . . . 14
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐴 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))))))) |
| 49 | 48 | pm2.43a 54 |
. . . . . . . . . . . . 13
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (𝐴 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))))) |
| 50 | 49 | com4r 94 |
. . . . . . . . . . . 12
⊢ (𝐴 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴)))))) |
| 51 | 50 | pm2.43i 52 |
. . . . . . . . . . 11
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))))) |
| 52 | 51 | 3imp 1111 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴) = ((𝐴 ·o 𝐵) +o ((𝐴 ·o 𝑦) +o 𝐴))) |
| 53 | 42, 52 | eqtr4d 2780 |
. . . . . . . . 9
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴)) |
| 54 | 39, 53 | eqeq12d 2753 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)) ↔ ((𝐴 ·o (𝐵 +o 𝑦)) +o 𝐴) = (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) +o 𝐴))) |
| 55 | 31, 54 | imbitrrid 246 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝑦 ∈ On) → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))) |
| 56 | 55 | 3exp 1120 |
. . . . . 6
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝑦 ∈ On → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))))) |
| 57 | 56 | com3r 87 |
. . . . 5
⊢ (𝑦 ∈ On → (𝐴 ∈ On → (𝐵 ∈ On → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦)))))) |
| 58 | 57 | impd 410 |
. . . 4
⊢ (𝑦 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o suc 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o suc 𝑦))))) |
| 59 | | vex 3484 |
. . . . . . . . . . . . . 14
⊢ 𝑥 ∈ V |
| 60 | | limelon 6448 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 ∈ V ∧ Lim 𝑥) → 𝑥 ∈ On) |
| 61 | 59, 60 | mpan 690 |
. . . . . . . . . . . . 13
⊢ (Lim
𝑥 → 𝑥 ∈ On) |
| 62 | | oacl 8573 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (𝐵 +o 𝑥) ∈ On) |
| 63 | | om0r 8577 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 +o 𝑥) ∈ On → (∅
·o (𝐵
+o 𝑥)) =
∅) |
| 64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅
·o (𝐵
+o 𝑥)) =
∅) |
| 65 | | om0r 8577 |
. . . . . . . . . . . . . . . 16
⊢ (𝐵 ∈ On → (∅
·o 𝐵) =
∅) |
| 66 | | om0r 8577 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ On → (∅
·o 𝑥) =
∅) |
| 67 | 65, 66 | oveqan12d 7450 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ((∅
·o 𝐵)
+o (∅ ·o 𝑥)) = (∅ +o
∅)) |
| 68 | | 0elon 6438 |
. . . . . . . . . . . . . . . 16
⊢ ∅
∈ On |
| 69 | | oa0 8554 |
. . . . . . . . . . . . . . . 16
⊢ (∅
∈ On → (∅ +o ∅) = ∅) |
| 70 | 68, 69 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ (∅
+o ∅) = ∅ |
| 71 | 67, 70 | eqtr2di 2794 |
. . . . . . . . . . . . . 14
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → ∅ =
((∅ ·o 𝐵) +o (∅
·o 𝑥))) |
| 72 | 64, 71 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((𝐵 ∈ On ∧ 𝑥 ∈ On) → (∅
·o (𝐵
+o 𝑥)) =
((∅ ·o 𝐵) +o (∅
·o 𝑥))) |
| 73 | 61, 72 | sylan2 593 |
. . . . . . . . . . . 12
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → (∅
·o (𝐵
+o 𝑥)) =
((∅ ·o 𝐵) +o (∅
·o 𝑥))) |
| 74 | 73 | ancoms 458 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (∅
·o (𝐵
+o 𝑥)) =
((∅ ·o 𝐵) +o (∅
·o 𝑥))) |
| 75 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → (𝐴 ·o (𝐵 +o 𝑥)) = (∅
·o (𝐵
+o 𝑥))) |
| 76 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (𝐴 ·o 𝐵) = (∅
·o 𝐵)) |
| 77 | | oveq1 7438 |
. . . . . . . . . . . . 13
⊢ (𝐴 = ∅ → (𝐴 ·o 𝑥) = (∅
·o 𝑥)) |
| 78 | 76, 77 | oveq12d 7449 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ((∅
·o 𝐵)
+o (∅ ·o 𝑥))) |
| 79 | 75, 78 | eqeq12d 2753 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ((𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) ↔ (∅ ·o
(𝐵 +o 𝑥)) = ((∅
·o 𝐵)
+o (∅ ·o 𝑥)))) |
| 80 | 74, 79 | imbitrrid 246 |
. . . . . . . . . 10
⊢ (𝐴 = ∅ → ((Lim 𝑥 ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))) |
| 81 | 80 | expd 415 |
. . . . . . . . 9
⊢ (𝐴 = ∅ → (Lim 𝑥 → (𝐵 ∈ On → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 82 | 81 | com3r 87 |
. . . . . . . 8
⊢ (𝐵 ∈ On → (𝐴 = ∅ → (Lim 𝑥 → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 83 | 82 | imp 406 |
. . . . . . 7
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))) |
| 84 | 83 | a1dd 50 |
. . . . . 6
⊢ ((𝐵 ∈ On ∧ 𝐴 = ∅) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 85 | | simplr 769 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝐵 ∈ On) |
| 86 | 62 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑥) ∈ On) |
| 87 | | onelon 6409 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐵 +o 𝑥) ∈ On ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On) |
| 88 | 86, 87 | sylan 580 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → 𝑧 ∈ On) |
| 89 | | ontri1 6418 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ¬ 𝑧 ∈ 𝐵)) |
| 90 | | oawordex 8595 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (𝐵 ⊆ 𝑧 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧)) |
| 91 | 89, 90 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 ∈ On ∧ 𝑧 ∈ On) → (¬ 𝑧 ∈ 𝐵 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧)) |
| 92 | 85, 88, 91 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (¬ 𝑧 ∈ 𝐵 ↔ ∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧)) |
| 93 | | oaord 8585 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑣 ∈ On ∧ 𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 ↔ (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 94 | 93 | 3expb 1121 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣 ∈ 𝑥 ↔ (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 95 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 +o 𝑣) = 𝑧 → ((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ↔ 𝑧 ∈ (𝐵 +o 𝑥))) |
| 96 | 94, 95 | sylan9bb 509 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑣 ∈ 𝑥 ↔ 𝑧 ∈ (𝐵 +o 𝑥))) |
| 97 | | iba 527 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 +o 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 98 | 97 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑣 ∈ 𝑥 ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 99 | 96, 98 | bitr3d 281 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑣 ∈ On ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) ∧ (𝐵 +o 𝑣) = 𝑧) → (𝑧 ∈ (𝐵 +o 𝑥) ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 100 | 99 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝑣 ∈ On ∧ (𝐵 +o 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑧 ∈ (𝐵 +o 𝑥) ↔ (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 101 | 100 | biimpcd 249 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑧 ∈ (𝐵 +o 𝑥) → (((𝑣 ∈ On ∧ (𝐵 +o 𝑣) = 𝑧) ∧ (𝑥 ∈ On ∧ 𝐵 ∈ On)) → (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 102 | 101 | exp4c 432 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑧 ∈ (𝐵 +o 𝑥) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))))) |
| 103 | 102 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑧 ∈ (𝐵 +o 𝑥) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))))) |
| 104 | 103 | imp 406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑣 ∈ On → ((𝐵 +o 𝑣) = 𝑧 → (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)))) |
| 105 | 104 | reximdvai 3165 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (∃𝑣 ∈ On (𝐵 +o 𝑣) = 𝑧 → ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 106 | 92, 105 | sylbid 240 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (¬ 𝑧 ∈ 𝐵 → ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 107 | 106 | orrd 864 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑥 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 108 | 61, 107 | sylanl1 680 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 109 | 108 | adantlrl 720 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 110 | 109 | adantlr 715 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → (𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧))) |
| 111 | | 0ellim 6447 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (Lim
𝑥 → ∅ ∈
𝑥) |
| 112 | | om00el 8614 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → (∅
∈ (𝐴
·o 𝑥)
↔ (∅ ∈ 𝐴
∧ ∅ ∈ 𝑥))) |
| 113 | 112 | biimprd 248 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅
∈ 𝐴 ∧ ∅
∈ 𝑥) → ∅
∈ (𝐴
·o 𝑥))) |
| 114 | 111, 113 | sylan2i 606 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ On ∧ 𝑥 ∈ On) → ((∅
∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·o 𝑥))) |
| 115 | 61, 114 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ Lim 𝑥) → ((∅ ∈ 𝐴 ∧ Lim 𝑥) → ∅ ∈ (𝐴 ·o 𝑥))) |
| 116 | 115 | exp4b 430 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → (Lim 𝑥 → ∅ ∈ (𝐴 ·o 𝑥))))) |
| 117 | 116 | com4r 94 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (Lim
𝑥 → (𝐴 ∈ On → (Lim 𝑥 → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·o 𝑥))))) |
| 118 | 117 | pm2.43a 54 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (Lim
𝑥 → (𝐴 ∈ On → (∅ ∈ 𝐴 → ∅ ∈ (𝐴 ·o 𝑥)))) |
| 119 | 118 | imp31 417 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ∅ ∈ (𝐴 ·o 𝑥)) |
| 120 | 119 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∅ ∈ (𝐴 ·o 𝑥))) |
| 121 | 120 | adantlrr 721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∅ ∈ (𝐴 ·o 𝑥))) |
| 122 | | omordi 8604 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝐵 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵))) |
| 123 | 122 | ancom1s 653 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵))) |
| 124 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ (𝐴 ·o 𝐵))) |
| 125 | 22 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅) ↔ (𝐴 ·o 𝑧) ⊆ (𝐴 ·o 𝐵))) |
| 126 | 124, 125 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝐴 ·o 𝐵) ∈ On → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 127 | 21, 126 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 128 | 127 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → ((𝐴 ·o 𝑧) ∈ (𝐴 ·o 𝐵) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 129 | 123, 128 | syld 47 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 130 | 129 | adantll 714 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 131 | 121, 130 | jcad 512 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → (∅ ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅)))) |
| 132 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = ∅ → ((𝐴 ·o 𝐵) +o 𝑤) = ((𝐴 ·o 𝐵) +o ∅)) |
| 133 | 132 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑤 = ∅ → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) ↔ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o ∅))) |
| 134 | 133 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ ((∅
∈ (𝐴
·o 𝑥)
∧ (𝐴
·o 𝑧)
⊆ ((𝐴
·o 𝐵)
+o ∅)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)) |
| 135 | 131, 134 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝑧 ∈ 𝐵 → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 136 | 135 | adantrr 717 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝑧 ∈ 𝐵 → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 137 | | omordi 8604 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ On ∧ 𝐴 ∈ On) ∧ ∅ ∈
𝐴) → (𝑣 ∈ 𝑥 → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥))) |
| 138 | 61, 137 | sylanl1 680 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → (𝑣 ∈ 𝑥 → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥))) |
| 139 | 138 | adantrd 491 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥))) |
| 140 | 139 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥))) |
| 141 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑣 → (𝐵 +o 𝑦) = (𝐵 +o 𝑣)) |
| 142 | 141 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑣 → (𝐴 ·o (𝐵 +o 𝑦)) = (𝐴 ·o (𝐵 +o 𝑣))) |
| 143 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = 𝑣 → (𝐴 ·o 𝑦) = (𝐴 ·o 𝑣)) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = 𝑣 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) |
| 145 | 142, 144 | eqeq12d 2753 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = 𝑣 → ((𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ↔ (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 146 | 145 | rspccv 3619 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(∀𝑦 ∈
𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝑣 ∈ 𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 147 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o (𝐵 +o 𝑣)) = (𝐴 ·o 𝑧)) |
| 148 | | eqeq1 2741 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐴 ·o (𝐵 +o 𝑣)) = (𝐴 ·o 𝑧) ↔ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧))) |
| 149 | 147, 148 | imbitrid 244 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐵 +o 𝑣) = 𝑧 → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧))) |
| 150 | | eqimss2 4043 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) = (𝐴 ·o 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) |
| 151 | 149, 150 | syl6 35 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)) → ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 152 | 151 | imim2i 16 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑣 ∈ 𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → (𝑣 ∈ 𝑥 → ((𝐵 +o 𝑣) = 𝑧 → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))) |
| 153 | 152 | impd 410 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑣 ∈ 𝑥 → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 154 | 146, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(∀𝑦 ∈
𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 155 | 154 | ad2antll 729 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 156 | 140, 155 | jcad 512 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ((𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))))) |
| 157 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑤 = (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) |
| 158 | 157 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑤 = (𝐴 ·o 𝑣) → ((𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) ↔ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 159 | 158 | rspcev 3622 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝐴 ·o 𝑣) ∈ (𝐴 ·o 𝑥) ∧ (𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)) |
| 160 | 156, 159 | syl6 35 |
. . . . . . . . . . . . . . . . . 18
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 161 | 160 | rexlimdvw 3160 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 162 | 161 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 163 | 136, 162 | jaod 860 |
. . . . . . . . . . . . . . 15
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 164 | 163 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ((𝑧 ∈ 𝐵 ∨ ∃𝑣 ∈ On (𝑣 ∈ 𝑥 ∧ (𝐵 +o 𝑣) = 𝑧)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤))) |
| 165 | 110, 164 | mpd 15 |
. . . . . . . . . . . . 13
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) ∧ 𝑧 ∈ (𝐵 +o 𝑥)) → ∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)) |
| 166 | 165 | ralrimiva 3146 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ∀𝑧 ∈ (𝐵 +o 𝑥)∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤)) |
| 167 | | iunss2 5049 |
. . . . . . . . . . . 12
⊢
(∀𝑧 ∈
(𝐵 +o 𝑥)∃𝑤 ∈ (𝐴 ·o 𝑥)(𝐴 ·o 𝑧) ⊆ ((𝐴 ·o 𝐵) +o 𝑤) → ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) ⊆ ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 168 | 166, 167 | syl 17 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) ⊆ ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 169 | | omordlim 8615 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣)) |
| 170 | 169 | ex 412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣))) |
| 171 | 59, 170 | mpanr1 703 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ On ∧ Lim 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣))) |
| 172 | 171 | ancoms 458 |
. . . . . . . . . . . . . . . . . 18
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝑤 ∈ (𝐴 ·o 𝑥) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣))) |
| 173 | 172 | imp 406 |
. . . . . . . . . . . . . . . . 17
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣)) |
| 174 | 173 | adantlrr 721 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣)) |
| 175 | 174 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣)) |
| 176 | | oaordi 8584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ On ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 177 | 61, 176 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → (𝑣 ∈ 𝑥 → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 178 | 177 | imp 406 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ 𝐵 ∈ On) ∧ 𝑣 ∈ 𝑥) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)) |
| 179 | 178 | adantlrl 720 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥)) |
| 180 | 179 | a1d 25 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 181 | 180 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → (𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥))) |
| 182 | | limord 6444 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (Lim
𝑥 → Ord 𝑥) |
| 183 | | ordelon 6408 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((Ord
𝑥 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ On) |
| 184 | 182, 183 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) → 𝑣 ∈ On) |
| 185 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐴 ∈ On ∧ 𝑣 ∈ On) → (𝐴 ·o 𝑣) ∈ On) |
| 186 | 185 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ On ∧ 𝐴 ∈ On) → (𝐴 ·o 𝑣) ∈ On) |
| 187 | 186 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o 𝑣) ∈ On) |
| 188 | 21 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o 𝐵) ∈ On) |
| 189 | | oaordi 8584 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝐴 ·o 𝑣) ∈ On ∧ (𝐴 ·o 𝐵) ∈ On) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 190 | 187, 188,
189 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 191 | 184, 190 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 192 | 191 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 193 | 192 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 194 | 145 | rspccva 3621 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((∀𝑦 ∈
𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ∧ 𝑣 ∈ 𝑥) → (𝐴 ·o (𝐵 +o 𝑣)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣))) |
| 195 | 194 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((∀𝑦 ∈
𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 196 | 195 | adantll 714 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ∈ ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑣)))) |
| 197 | 193, 196 | sylibrd 259 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 198 | | oacl 8573 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 ∈ On ∧ 𝑣 ∈ On) → (𝐵 +o 𝑣) ∈ On) |
| 199 | 198 | ancoms 458 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑣 ∈ On ∧ 𝐵 ∈ On) → (𝐵 +o 𝑣) ∈ On) |
| 200 | | omcl 8574 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝐴 ∈ On ∧ (𝐵 +o 𝑣) ∈ On) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On) |
| 201 | 199, 200 | sylan2 593 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝐴 ∈ On ∧ (𝑣 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On) |
| 202 | 201 | an12s 649 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑣 ∈ On ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On) |
| 203 | 184, 202 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((Lim
𝑥 ∧ 𝑣 ∈ 𝑥) ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On) |
| 204 | 203 | an32s 652 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (𝐴 ·o (𝐵 +o 𝑣)) ∈ On) |
| 205 | | onelss 6426 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝐴 ·o (𝐵 +o 𝑣)) ∈ On → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 206 | 204, 205 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 207 | 206 | adantlr 715 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (((𝐴 ·o 𝐵) +o 𝑤) ∈ (𝐴 ·o (𝐵 +o 𝑣)) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 208 | 197, 207 | syld 47 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 209 | 181, 208 | jcad 512 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ∧ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))))) |
| 210 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝐵 +o 𝑣) → (𝐴 ·o 𝑧) = (𝐴 ·o (𝐵 +o 𝑣))) |
| 211 | 210 | sseq2d 4016 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝐵 +o 𝑣) → (((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧) ↔ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣)))) |
| 212 | 211 | rspcev 3622 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝐵 +o 𝑣) ∈ (𝐵 +o 𝑥) ∧ ((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o (𝐵 +o 𝑣))) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)) |
| 213 | 209, 212 | syl6 35 |
. . . . . . . . . . . . . . . . 17
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑣 ∈ 𝑥) → (𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))) |
| 214 | 213 | rexlimdva 3155 |
. . . . . . . . . . . . . . . 16
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → (∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))) |
| 215 | 214 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → (∃𝑣 ∈ 𝑥 𝑤 ∈ (𝐴 ·o 𝑣) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧))) |
| 216 | 175, 215 | mpd 15 |
. . . . . . . . . . . . . 14
⊢ ((((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) ∧ 𝑤 ∈ (𝐴 ·o 𝑥)) → ∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)) |
| 217 | 216 | ralrimiva 3146 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → ∀𝑤 ∈ (𝐴 ·o 𝑥)∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧)) |
| 218 | | iunss2 5049 |
. . . . . . . . . . . . 13
⊢
(∀𝑤 ∈
(𝐴 ·o
𝑥)∃𝑧 ∈ (𝐵 +o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ (𝐴 ·o 𝑧) → ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 219 | 217, 218 | syl 17 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦))) → ∪ 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 220 | 219 | adantrl 716 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ∪ 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤) ⊆ ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 221 | 168, 220 | eqssd 4001 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ∪ 𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧) = ∪ 𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 222 | | oalimcl 8598 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐵 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) → Lim (𝐵 +o 𝑥)) |
| 223 | 59, 222 | mpanr1 703 |
. . . . . . . . . . . . . . 15
⊢ ((𝐵 ∈ On ∧ Lim 𝑥) → Lim (𝐵 +o 𝑥)) |
| 224 | 223 | ancoms 458 |
. . . . . . . . . . . . . 14
⊢ ((Lim
𝑥 ∧ 𝐵 ∈ On) → Lim (𝐵 +o 𝑥)) |
| 225 | 224 | anim2i 617 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ (Lim 𝑥 ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥))) |
| 226 | 225 | an12s 649 |
. . . . . . . . . . . 12
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥))) |
| 227 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝐵 +o 𝑥) ∈ V |
| 228 | | omlim 8571 |
. . . . . . . . . . . . 13
⊢ ((𝐴 ∈ On ∧ ((𝐵 +o 𝑥) ∈ V ∧ Lim (𝐵 +o 𝑥))) → (𝐴 ·o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 229 | 227, 228 | mpanr1 703 |
. . . . . . . . . . . 12
⊢ ((𝐴 ∈ On ∧ Lim (𝐵 +o 𝑥)) → (𝐴 ·o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 230 | 226, 229 | syl 17 |
. . . . . . . . . . 11
⊢ ((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) → (𝐴 ·o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 231 | 230 | adantr 480 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝐴 ·o (𝐵 +o 𝑥)) = ∪
𝑧 ∈ (𝐵 +o 𝑥)(𝐴 ·o 𝑧)) |
| 232 | 21 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → (𝐴 ·o 𝐵) ∈ On) |
| 233 | 59 | jctl 523 |
. . . . . . . . . . . . . . . 16
⊢ (Lim
𝑥 → (𝑥 ∈ V ∧ Lim 𝑥)) |
| 234 | 233 | anim1ci 616 |
. . . . . . . . . . . . . . 15
⊢ ((Lim
𝑥 ∧ 𝐴 ∈ On) → (𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥))) |
| 235 | | omlimcl 8616 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ (𝑥 ∈ V ∧ Lim 𝑥)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥)) |
| 236 | 234, 235 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((Lim
𝑥 ∧ 𝐴 ∈ On) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥)) |
| 237 | 236 | adantlrr 721 |
. . . . . . . . . . . . 13
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → Lim (𝐴 ·o 𝑥)) |
| 238 | | ovex 7464 |
. . . . . . . . . . . . 13
⊢ (𝐴 ·o 𝑥) ∈ V |
| 239 | 237, 238 | jctil 519 |
. . . . . . . . . . . 12
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝑥) ∈ V ∧ Lim (𝐴 ·o 𝑥))) |
| 240 | | oalim 8570 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·o 𝐵) ∈ On ∧ ((𝐴 ·o 𝑥) ∈ V ∧ Lim (𝐴 ·o 𝑥))) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 241 | 232, 239,
240 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ ∅ ∈ 𝐴) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 242 | 241 | adantrr 717 |
. . . . . . . . . 10
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)) = ∪
𝑤 ∈ (𝐴 ·o 𝑥)((𝐴 ·o 𝐵) +o 𝑤)) |
| 243 | 221, 231,
242 | 3eqtr4d 2787 |
. . . . . . . . 9
⊢ (((Lim
𝑥 ∧ (𝐴 ∈ On ∧ 𝐵 ∈ On)) ∧ (∅ ∈ 𝐴 ∧ ∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)))) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))) |
| 244 | 243 | exp43 436 |
. . . . . . . 8
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 →
(∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))) |
| 245 | 244 | com3l 89 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∅
∈ 𝐴 → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥)))))) |
| 246 | 245 | imp 406 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ ∅ ∈
𝐴) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 247 | 84, 246 | oe0lem 8551 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (Lim 𝑥 → (∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 248 | 247 | com12 32 |
. . . 4
⊢ (Lim
𝑥 → ((𝐴 ∈ On ∧ 𝐵 ∈ On) →
(∀𝑦 ∈ 𝑥 (𝐴 ·o (𝐵 +o 𝑦)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑦)) → (𝐴 ·o (𝐵 +o 𝑥)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝑥))))) |
| 249 | 5, 10, 15, 20, 30, 58, 248 | tfinds3 7886 |
. . 3
⊢ (𝐶 ∈ On → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶)))) |
| 250 | 249 | expdcom 414 |
. 2
⊢ (𝐴 ∈ On → (𝐵 ∈ On → (𝐶 ∈ On → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))))) |
| 251 | 250 | 3imp 1111 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On ∧ 𝐶 ∈ On) → (𝐴 ·o (𝐵 +o 𝐶)) = ((𝐴 ·o 𝐵) +o (𝐴 ·o 𝐶))) |