| Step | Hyp | Ref
| Expression |
| 1 | | omex 9683 |
. . . . 5
⊢ ω
∈ V |
| 2 | 1 | 0dom 9146 |
. . . 4
⊢ ∅
≼ ω |
| 3 | | breq1 5146 |
. . . 4
⊢ (∪ 𝐴 =
∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼
ω)) |
| 4 | 2, 3 | mpbiri 258 |
. . 3
⊢ (∪ 𝐴 =
∅ → ∪ 𝐴 ≼ ω) |
| 5 | 4 | a1d 25 |
. 2
⊢ (∪ 𝐴 =
∅ → ((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
| 6 | | n0 4353 |
. . 3
⊢ (∪ 𝐴
≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴) |
| 7 | | ne0i 4341 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ∪ 𝐴
→ ∪ 𝐴 ≠ ∅) |
| 8 | | unieq 4918 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
| 9 | | uni0 4935 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
| 10 | 8, 9 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
| 11 | 10 | necon3i 2973 |
. . . . . . . . . 10
⊢ (∪ 𝐴
≠ ∅ → 𝐴 ≠
∅) |
| 12 | 7, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝐴
→ 𝐴 ≠
∅) |
| 13 | 12 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅) |
| 14 | | simpl1 1192 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω) |
| 15 | | ctex 9004 |
. . . . . . . . 9
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
| 16 | | 0sdomg 9144 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 17 | 14, 15, 16 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
| 18 | 13, 17 | mpbird 257 |
. . . . . . 7
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴) |
| 19 | | fodomr 9168 |
. . . . . . 7
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ω) →
∃𝑏 𝑏:ω–onto→𝐴) |
| 20 | 18, 14, 19 | syl2anc 584 |
. . . . . 6
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴) |
| 21 | | omelon 9686 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
| 22 | | onenon 9989 |
. . . . . . . . . . . 12
⊢ (ω
∈ On → ω ∈ dom card) |
| 23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ω
∈ dom card |
| 24 | | xpnum 9991 |
. . . . . . . . . . 11
⊢ ((ω
∈ dom card ∧ ω ∈ dom card) → (ω × ω)
∈ dom card) |
| 25 | 23, 23, 24 | mp2an 692 |
. . . . . . . . . 10
⊢ (ω
× ω) ∈ dom card |
| 26 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto→𝐴) |
| 27 | | fof 6820 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴) |
| 28 | 26, 27 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴) |
| 29 | | simprl 771 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω) |
| 30 | 28, 29 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴) |
| 32 | | elssuni 4937 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑓) ∈ 𝐴 → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
| 33 | 31, 32 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
| 34 | 30, 32 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
| 35 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or ∪ 𝐴) |
| 36 | | soss 5612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏‘𝑓) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑓))) |
| 37 | 34, 35, 36 | sylc 65 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏‘𝑓)) |
| 38 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin) |
| 39 | 38, 30 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin) |
| 40 | | finnisoeu 10153 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
| 41 | 37, 39, 40 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
| 42 | | iotacl 6547 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}) |
| 43 | 41, 42 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}) |
| 44 | | iotaex 6534 |
. . . . . . . . . . . . . . . . . . 19
⊢
(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V |
| 45 | | isoeq1 7337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))) |
| 46 | | isoeq1 7337 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))) |
| 47 | 46 | cbvabv 2812 |
. . . . . . . . . . . . . . . . . . 19
⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} |
| 48 | 44, 45, 47 | elab2 3682 |
. . . . . . . . . . . . . . . . . 18
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
| 49 | 43, 48 | sylib 218 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
| 50 | | isof1o 7343 |
. . . . . . . . . . . . . . . . 17
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓)) |
| 51 | | f1of 6848 |
. . . . . . . . . . . . . . . . 17
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓)) |
| 52 | 49, 50, 51 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓)) |
| 53 | 52 | ffvelcdmda 7104 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓)) |
| 54 | 33, 53 | sseldd 3984 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ ∪ 𝐴) |
| 55 | | simprl 771 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → 𝑎 ∈ ∪ 𝐴) |
| 56 | 55 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏‘𝑓))) → 𝑎 ∈ ∪ 𝐴) |
| 57 | 54, 56 | ifclda 4561 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴) |
| 58 | 57 | ralrimivva 3202 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴) |
| 59 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) |
| 60 | 59 | fmpo 8093 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
ω ∀𝑔 ∈
ω if(𝑔 ∈
(card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴) |
| 61 | 58, 60 | sylib 218 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴) |
| 62 | | eluni 4910 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ∪ 𝐴
↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) |
| 63 | | simplrr 778 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴) |
| 64 | | simprr 773 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴) |
| 65 | | foelrn 7127 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗)) |
| 66 | 63, 64, 65 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗)) |
| 67 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω) |
| 68 | | ordom 7897 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Ord
ω |
| 69 | | simpll2 1214 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐴 ⊆ Fin) |
| 70 | | simplrr 778 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω–onto→𝐴) |
| 71 | 70, 27 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω⟶𝐴) |
| 72 | 71, 67 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴) |
| 73 | 69, 72 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin) |
| 74 | | ficardom 10001 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω) |
| 75 | 73, 74 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω) |
| 76 | | ordelss 6400 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord
ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω) |
| 77 | 68, 75, 76 | sylancr 587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω) |
| 78 | | elssuni 4937 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴) |
| 79 | 72, 78 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴) |
| 80 | | simpll3 1215 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴) |
| 81 | | soss 5612 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗))) |
| 82 | 79, 80, 81 | sylc 65 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗)) |
| 83 | | finnisoeu 10153 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
| 84 | 82, 73, 83 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
| 85 | | iotacl 6547 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}) |
| 86 | 84, 85 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}) |
| 87 | | iotaex 6534 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V |
| 88 | | isoeq1 7337 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 89 | | isoeq1 7337 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 90 | 89 | cbvabv 2812 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} |
| 91 | 87, 88, 90 | elab2 3682 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
| 92 | 86, 91 | sylib 218 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
| 93 | | isof1o 7343 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗)) |
| 94 | 92, 93 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗)) |
| 95 | | f1ocnv 6860 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗))) |
| 96 | | f1of 6848 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗))) |
| 97 | 94, 95, 96 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗))) |
| 98 | | simprll 779 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ 𝑖) |
| 99 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑖 = (𝑏‘𝑗)) |
| 100 | 98, 99 | eleqtrd 2843 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗)) |
| 101 | 97, 100 | ffvelcdmd 7105 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))) |
| 102 | 77, 101 | sseldd 3984 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) |
| 103 | | 2fveq3 6911 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗))) |
| 104 | 103 | eleq2d 2827 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗)))) |
| 105 | | isoeq4 7340 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)))) |
| 106 | 103, 105 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)))) |
| 107 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗)) |
| 108 | | isoeq5 7341 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏‘𝑓) = (𝑏‘𝑗) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 109 | 107, 108 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 110 | 106, 109 | bitrd 279 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 111 | 110 | iotabidv 6545 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
| 112 | 111 | fveq1d 6908 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔)) |
| 113 | 104, 112 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎)) |
| 114 | | eleq1 2829 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))) |
| 115 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
| 116 | 114, 115 | ifbieq1d 4550 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
| 117 | | fvex 6919 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V |
| 118 | | vex 3484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑎 ∈ V |
| 119 | 117, 118 | ifex 4576 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V |
| 120 | 113, 116,
59, 119 | ovmpo 7593 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ω ∧ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
| 121 | 67, 102, 120 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
| 122 | 101 | iftrued 4533 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
| 123 | | f1ocnvfv2 7297 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) ∧ 𝑐 ∈ (𝑏‘𝑗)) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐) |
| 124 | 94, 100, 123 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐) |
| 125 | 121, 122,
124 | 3eqtrrd 2782 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
| 126 | | rspceov 7480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ω ∧ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
| 127 | 67, 102, 125, 126 | syl3anc 1373 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
| 128 | 127 | expr 456 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 129 | 128 | expd 415 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))) |
| 130 | 129 | rexlimdv 3153 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 131 | 66, 130 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
| 132 | 131 | ex 412 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 133 | 132 | exlimdv 1933 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 134 | 62, 133 | biimtrid 242 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑐 ∈ ∪ 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 135 | 134 | ralrimiv 3145 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
| 136 | | foov 7607 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴
∧ ∀𝑐 ∈
∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
| 137 | 61, 135, 136 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴) |
| 138 | | fodomnum 10097 |
. . . . . . . . . 10
⊢ ((ω
× ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴
≼ (ω × ω))) |
| 139 | 25, 137, 138 | mpsyl 68 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω ×
ω)) |
| 140 | | xpomen 10055 |
. . . . . . . . 9
⊢ (ω
× ω) ≈ ω |
| 141 | | domentr 9053 |
. . . . . . . . 9
⊢ ((∪ 𝐴
≼ (ω × ω) ∧ (ω × ω) ≈
ω) → ∪ 𝐴 ≼ ω) |
| 142 | 139, 140,
141 | sylancl 586 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼
ω) |
| 143 | 142 | expr 456 |
. . . . . . 7
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼
ω)) |
| 144 | 143 | exlimdv 1933 |
. . . . . 6
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∃𝑏 𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼
ω)) |
| 145 | 20, 144 | mpd 15 |
. . . . 5
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∪ 𝐴
≼ ω) |
| 146 | 145 | expcom 413 |
. . . 4
⊢ (𝑎 ∈ ∪ 𝐴
→ ((𝐴 ≼ ω
∧ 𝐴 ⊆ Fin ∧
𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
| 147 | 146 | exlimiv 1930 |
. . 3
⊢
(∃𝑎 𝑎 ∈ ∪ 𝐴
→ ((𝐴 ≼ ω
∧ 𝐴 ⊆ Fin ∧
𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
| 148 | 6, 147 | sylbi 217 |
. 2
⊢ (∪ 𝐴
≠ ∅ → ((𝐴
≼ ω ∧ 𝐴
⊆ Fin ∧ 𝐵 Or
∪ 𝐴) → ∪ 𝐴 ≼
ω)) |
| 149 | 5, 148 | pm2.61ine 3025 |
1
⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) → ∪ 𝐴
≼ ω) |