| Step | Hyp | Ref
| Expression |
| 1 | | omelon 9686 |
. . . . 5
⊢ ω
∈ On |
| 2 | | omcl 8574 |
. . . . 5
⊢ ((𝐴 ∈ On ∧ ω ∈
On) → (𝐴
·o ω) ∈ On) |
| 3 | 1, 2 | mpan2 691 |
. . . 4
⊢ (𝐴 ∈ On → (𝐴 ·o ω)
∈ On) |
| 4 | | oawordex 8595 |
. . . 4
⊢ (((𝐴 ·o ω)
∈ On ∧ 𝐵 ∈
On) → ((𝐴
·o ω) ⊆ 𝐵 ↔ ∃𝑥 ∈ On ((𝐴 ·o ω) +o
𝑥) = 𝐵)) |
| 5 | 3, 4 | sylan 580 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o ω)
⊆ 𝐵 ↔
∃𝑥 ∈ On ((𝐴 ·o ω)
+o 𝑥) = 𝐵)) |
| 6 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐴 ∈ On) |
| 7 | 6 | adantr 480 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → 𝐴 ∈ On) |
| 8 | 3 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → (𝐴 ·o ω)
∈ On) |
| 9 | | simpr 484 |
. . . . . . 7
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → 𝑥 ∈ On) |
| 10 | | oaass 8599 |
. . . . . . 7
⊢ ((𝐴 ∈ On ∧ (𝐴 ·o ω)
∈ On ∧ 𝑥 ∈
On) → ((𝐴
+o (𝐴
·o ω)) +o 𝑥) = (𝐴 +o ((𝐴 ·o ω) +o
𝑥))) |
| 11 | 7, 8, 9, 10 | syl3anc 1373 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → ((𝐴 +o (𝐴 ·o ω))
+o 𝑥) = (𝐴 +o ((𝐴 ·o ω)
+o 𝑥))) |
| 12 | | 1on 8518 |
. . . . . . . . . 10
⊢
1o ∈ On |
| 13 | | odi 8617 |
. . . . . . . . . 10
⊢ ((𝐴 ∈ On ∧ 1o
∈ On ∧ ω ∈ On) → (𝐴 ·o (1o
+o ω)) = ((𝐴 ·o 1o)
+o (𝐴
·o ω))) |
| 14 | 12, 1, 13 | mp3an23 1455 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 ·o
(1o +o ω)) = ((𝐴 ·o 1o)
+o (𝐴
·o ω))) |
| 15 | | 1oaomeqom 43306 |
. . . . . . . . . . 11
⊢
(1o +o ω) = ω |
| 16 | 15 | oveq2i 7442 |
. . . . . . . . . 10
⊢ (𝐴 ·o
(1o +o ω)) = (𝐴 ·o
ω) |
| 17 | 16 | a1i 11 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 ·o
(1o +o ω)) = (𝐴 ·o
ω)) |
| 18 | | om1 8580 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝐴 ·o
1o) = 𝐴) |
| 19 | 18 | oveq1d 7446 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → ((𝐴 ·o
1o) +o (𝐴 ·o ω)) = (𝐴 +o (𝐴 ·o
ω))) |
| 20 | 14, 17, 19 | 3eqtr3rd 2786 |
. . . . . . . 8
⊢ (𝐴 ∈ On → (𝐴 +o (𝐴 ·o ω))
= (𝐴 ·o
ω)) |
| 21 | 20 | oveq1d 7446 |
. . . . . . 7
⊢ (𝐴 ∈ On → ((𝐴 +o (𝐴 ·o ω))
+o 𝑥) = ((𝐴 ·o ω)
+o 𝑥)) |
| 22 | 21 | ad2antrr 726 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → ((𝐴 +o (𝐴 ·o ω))
+o 𝑥) = ((𝐴 ·o ω)
+o 𝑥)) |
| 23 | 11, 22 | eqtr3d 2779 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → (𝐴 +o ((𝐴 ·o ω)
+o 𝑥)) = ((𝐴 ·o ω)
+o 𝑥)) |
| 24 | | oveq2 7439 |
. . . . . 6
⊢ (((𝐴 ·o ω)
+o 𝑥) = 𝐵 → (𝐴 +o ((𝐴 ·o ω) +o
𝑥)) = (𝐴 +o 𝐵)) |
| 25 | | id 22 |
. . . . . 6
⊢ (((𝐴 ·o ω)
+o 𝑥) = 𝐵 → ((𝐴 ·o ω) +o
𝑥) = 𝐵) |
| 26 | 24, 25 | eqeq12d 2753 |
. . . . 5
⊢ (((𝐴 ·o ω)
+o 𝑥) = 𝐵 → ((𝐴 +o ((𝐴 ·o ω) +o
𝑥)) = ((𝐴 ·o ω) +o
𝑥) ↔ (𝐴 +o 𝐵) = 𝐵)) |
| 27 | 23, 26 | syl5ibcom 245 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑥 ∈ On) → (((𝐴 ·o ω)
+o 𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
| 28 | 27 | rexlimdva 3155 |
. . 3
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (∃𝑥 ∈ On ((𝐴 ·o ω) +o
𝑥) = 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
| 29 | 5, 28 | sylbid 240 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o ω)
⊆ 𝐵 → (𝐴 +o 𝐵) = 𝐵)) |
| 30 | | limom 7903 |
. . . . . 6
⊢ Lim
ω |
| 31 | | omlim 8571 |
. . . . . 6
⊢ ((𝐴 ∈ On ∧ (ω ∈
On ∧ Lim ω)) → (𝐴 ·o ω) = ∪ 𝑥 ∈ ω (𝐴 ·o 𝑥)) |
| 32 | 1, 30, 31 | mpanr12 705 |
. . . . 5
⊢ (𝐴 ∈ On → (𝐴 ·o ω) =
∪ 𝑥 ∈ ω (𝐴 ·o 𝑥)) |
| 33 | 32 | ad2antrr 726 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 ·o ω) = ∪ 𝑥 ∈ ω (𝐴 ·o 𝑥)) |
| 34 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = ∅ → (𝐴 ·o 𝑥) = (𝐴 ·o
∅)) |
| 35 | 34 | sseq1d 4015 |
. . . . . . . 8
⊢ (𝑥 = ∅ → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ (𝐴 ·o ∅) ⊆ 𝐵)) |
| 36 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o 𝑦)) |
| 37 | 36 | sseq1d 4015 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ (𝐴 ·o 𝑦) ⊆ 𝐵)) |
| 38 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = suc 𝑦 → (𝐴 ·o 𝑥) = (𝐴 ·o suc 𝑦)) |
| 39 | 38 | sseq1d 4015 |
. . . . . . . 8
⊢ (𝑥 = suc 𝑦 → ((𝐴 ·o 𝑥) ⊆ 𝐵 ↔ (𝐴 ·o suc 𝑦) ⊆ 𝐵)) |
| 40 | | om0 8555 |
. . . . . . . . . 10
⊢ (𝐴 ∈ On → (𝐴 ·o ∅) =
∅) |
| 41 | | 0ss 4400 |
. . . . . . . . . 10
⊢ ∅
⊆ 𝐵 |
| 42 | 40, 41 | eqsstrdi 4028 |
. . . . . . . . 9
⊢ (𝐴 ∈ On → (𝐴 ·o ∅)
⊆ 𝐵) |
| 43 | 42 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 ·o ∅) ⊆ 𝐵) |
| 44 | | nnon 7893 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ω → 𝑦 ∈ On) |
| 45 | | omcl 8574 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ On) → (𝐴 ·o 𝑦) ∈ On) |
| 46 | 6, 44, 45 | syl2an 596 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ ω) → (𝐴 ·o 𝑦) ∈ On) |
| 47 | | simpr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → 𝐵 ∈ On) |
| 48 | 47 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ ω) → 𝐵 ∈ On) |
| 49 | 6 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ ω) → 𝐴 ∈ On) |
| 50 | 46, 48, 49 | 3jca 1129 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ 𝑦 ∈ ω) → ((𝐴 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On)) |
| 51 | 50 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On))) |
| 52 | 51 | adantrd 491 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → ((𝐴 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On))) |
| 53 | 52 | imp 406 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) → ((𝐴 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On)) |
| 54 | | oaword 8587 |
. . . . . . . . . . . 12
⊢ (((𝐴 ·o 𝑦) ∈ On ∧ 𝐵 ∈ On ∧ 𝐴 ∈ On) → ((𝐴 ·o 𝑦) ⊆ 𝐵 ↔ (𝐴 +o (𝐴 ·o 𝑦)) ⊆ (𝐴 +o 𝐵))) |
| 55 | 53, 54 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) → ((𝐴 ·o 𝑦) ⊆ 𝐵 ↔ (𝐴 +o (𝐴 ·o 𝑦)) ⊆ (𝐴 +o 𝐵))) |
| 56 | 55 | biimpa 476 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) ∧ (𝐴 ·o 𝑦) ⊆ 𝐵) → (𝐴 +o (𝐴 ·o 𝑦)) ⊆ (𝐴 +o 𝐵)) |
| 57 | | simpl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → 𝐴 ∈ On) |
| 58 | 12 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) →
1o ∈ On) |
| 59 | 44 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → 𝑦 ∈ On) |
| 60 | | odi 8617 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝐴 ∈ On ∧ 1o
∈ On ∧ 𝑦 ∈
On) → (𝐴
·o (1o +o 𝑦)) = ((𝐴 ·o 1o)
+o (𝐴
·o 𝑦))) |
| 61 | 57, 58, 59, 60 | syl3anc 1373 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → (𝐴 ·o
(1o +o 𝑦)) = ((𝐴 ·o 1o)
+o (𝐴
·o 𝑦))) |
| 62 | | 1onn 8678 |
. . . . . . . . . . . . . . . . . . . 20
⊢
1o ∈ ω |
| 63 | | nnacom 8655 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((1o ∈ ω ∧ 𝑦 ∈ ω) → (1o
+o 𝑦) = (𝑦 +o
1o)) |
| 64 | 62, 63 | mpan 690 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω →
(1o +o 𝑦) = (𝑦 +o
1o)) |
| 65 | | oa1suc 8569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 ∈ On → (𝑦 +o 1o) =
suc 𝑦) |
| 66 | 44, 65 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 ∈ ω → (𝑦 +o 1o) =
suc 𝑦) |
| 67 | 64, 66 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 ∈ ω →
(1o +o 𝑦) = suc 𝑦) |
| 68 | 67 | oveq2d 7447 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 ∈ ω → (𝐴 ·o
(1o +o 𝑦)) = (𝐴 ·o suc 𝑦)) |
| 69 | 68 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → (𝐴 ·o
(1o +o 𝑦)) = (𝐴 ·o suc 𝑦)) |
| 70 | 18 | oveq1d 7446 |
. . . . . . . . . . . . . . . . 17
⊢ (𝐴 ∈ On → ((𝐴 ·o
1o) +o (𝐴 ·o 𝑦)) = (𝐴 +o (𝐴 ·o 𝑦))) |
| 71 | 70 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → ((𝐴 ·o
1o) +o (𝐴 ·o 𝑦)) = (𝐴 +o (𝐴 ·o 𝑦))) |
| 72 | 61, 69, 71 | 3eqtr3rd 2786 |
. . . . . . . . . . . . . . 15
⊢ ((𝐴 ∈ On ∧ 𝑦 ∈ ω) → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦)) |
| 73 | 72 | expcom 413 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ω → (𝐴 ∈ On → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦))) |
| 74 | 73 | adantrd 491 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ω → ((𝐴 ∈ On ∧ 𝐵 ∈ On) → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦))) |
| 75 | 74 | adantrd 491 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ω → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦))) |
| 76 | 75 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦)) |
| 77 | 76 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) ∧ (𝐴 ·o 𝑦) ⊆ 𝐵) → (𝐴 +o (𝐴 ·o 𝑦)) = (𝐴 ·o suc 𝑦)) |
| 78 | | simpr 484 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 +o 𝐵) = 𝐵) |
| 79 | 78 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) → (𝐴 +o 𝐵) = 𝐵) |
| 80 | 79 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) ∧ (𝐴 ·o 𝑦) ⊆ 𝐵) → (𝐴 +o 𝐵) = 𝐵) |
| 81 | 56, 77, 80 | 3sstr3d 4038 |
. . . . . . . . 9
⊢ (((𝑦 ∈ ω ∧ ((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵)) ∧ (𝐴 ·o 𝑦) ⊆ 𝐵) → (𝐴 ·o suc 𝑦) ⊆ 𝐵) |
| 82 | 81 | exp31 419 |
. . . . . . . 8
⊢ (𝑦 ∈ ω → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → ((𝐴 ·o 𝑦) ⊆ 𝐵 → (𝐴 ·o suc 𝑦) ⊆ 𝐵))) |
| 83 | 35, 37, 39, 43, 82 | finds2 7920 |
. . . . . . 7
⊢ (𝑥 ∈ ω → (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 ·o 𝑥) ⊆ 𝐵)) |
| 84 | 83 | com12 32 |
. . . . . 6
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝑥 ∈ ω → (𝐴 ·o 𝑥) ⊆ 𝐵)) |
| 85 | 84 | ralrimiv 3145 |
. . . . 5
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → ∀𝑥 ∈ ω (𝐴 ·o 𝑥) ⊆ 𝐵) |
| 86 | | iunss 5045 |
. . . . 5
⊢ (∪ 𝑥 ∈ ω (𝐴 ·o 𝑥) ⊆ 𝐵 ↔ ∀𝑥 ∈ ω (𝐴 ·o 𝑥) ⊆ 𝐵) |
| 87 | 85, 86 | sylibr 234 |
. . . 4
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → ∪
𝑥 ∈ ω (𝐴 ·o 𝑥) ⊆ 𝐵) |
| 88 | 33, 87 | eqsstrd 4018 |
. . 3
⊢ (((𝐴 ∈ On ∧ 𝐵 ∈ On) ∧ (𝐴 +o 𝐵) = 𝐵) → (𝐴 ·o ω) ⊆ 𝐵) |
| 89 | 88 | ex 412 |
. 2
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 +o 𝐵) = 𝐵 → (𝐴 ·o ω) ⊆ 𝐵)) |
| 90 | 29, 89 | impbid 212 |
1
⊢ ((𝐴 ∈ On ∧ 𝐵 ∈ On) → ((𝐴 ·o ω)
⊆ 𝐵 ↔ (𝐴 +o 𝐵) = 𝐵)) |