Step | Hyp | Ref
| Expression |
1 | | omex 8423 |
. . . . 5
⊢ ω
∈ V |
2 | 1 | 0dom 7975 |
. . . 4
⊢ ∅
≼ ω |
3 | | breq1 4586 |
. . . 4
⊢ (∪ 𝐴 =
∅ → (∪ 𝐴 ≼ ω ↔ ∅ ≼
ω)) |
4 | 2, 3 | mpbiri 247 |
. . 3
⊢ (∪ 𝐴 =
∅ → ∪ 𝐴 ≼ ω) |
5 | 4 | a1d 25 |
. 2
⊢ (∪ 𝐴 =
∅ → ((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
6 | | n0 3890 |
. . 3
⊢ (∪ 𝐴
≠ ∅ ↔ ∃𝑎 𝑎 ∈ ∪ 𝐴) |
7 | | ne0i 3880 |
. . . . . . . . . 10
⊢ (𝑎 ∈ ∪ 𝐴
→ ∪ 𝐴 ≠ ∅) |
8 | | unieq 4380 |
. . . . . . . . . . . 12
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∪ ∅) |
9 | | uni0 4401 |
. . . . . . . . . . . 12
⊢ ∪ ∅ = ∅ |
10 | 8, 9 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (𝐴 = ∅ → ∪ 𝐴 =
∅) |
11 | 10 | necon3i 2814 |
. . . . . . . . . 10
⊢ (∪ 𝐴
≠ ∅ → 𝐴 ≠
∅) |
12 | 7, 11 | syl 17 |
. . . . . . . . 9
⊢ (𝑎 ∈ ∪ 𝐴
→ 𝐴 ≠
∅) |
13 | 12 | adantl 481 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≠ ∅) |
14 | | simpl1 1057 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → 𝐴 ≼ ω) |
15 | | reldom 7847 |
. . . . . . . . . 10
⊢ Rel
≼ |
16 | 15 | brrelexi 5082 |
. . . . . . . . 9
⊢ (𝐴 ≼ ω → 𝐴 ∈ V) |
17 | | 0sdomg 7974 |
. . . . . . . . 9
⊢ (𝐴 ∈ V → (∅
≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
18 | 14, 16, 17 | 3syl 18 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∅ ≺ 𝐴 ↔ 𝐴 ≠ ∅)) |
19 | 13, 18 | mpbird 246 |
. . . . . . 7
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∅ ≺ 𝐴) |
20 | | fodomr 7996 |
. . . . . . 7
⊢ ((∅
≺ 𝐴 ∧ 𝐴 ≼ ω) →
∃𝑏 𝑏:ω–onto→𝐴) |
21 | 19, 14, 20 | syl2anc 691 |
. . . . . 6
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∃𝑏 𝑏:ω–onto→𝐴) |
22 | | omelon 8426 |
. . . . . . . . . . . 12
⊢ ω
∈ On |
23 | | onenon 8658 |
. . . . . . . . . . . 12
⊢ (ω
∈ On → ω ∈ dom card) |
24 | 22, 23 | ax-mp 5 |
. . . . . . . . . . 11
⊢ ω
∈ dom card |
25 | | xpnum 8660 |
. . . . . . . . . . 11
⊢ ((ω
∈ dom card ∧ ω ∈ dom card) → (ω × ω)
∈ dom card) |
26 | 24, 24, 25 | mp2an 704 |
. . . . . . . . . 10
⊢ (ω
× ω) ∈ dom card |
27 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω–onto→𝐴) |
28 | | fof 6028 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏:ω–onto→𝐴 → 𝑏:ω⟶𝐴) |
29 | 27, 28 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑏:ω⟶𝐴) |
30 | | simprl 790 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝑓 ∈ ω) |
31 | 29, 30 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ 𝐴) |
32 | 31 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ∈ 𝐴) |
33 | | elssuni 4403 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑏‘𝑓) ∈ 𝐴 → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
34 | 32, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
35 | 31, 33 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ⊆ ∪ 𝐴) |
36 | | simpll3 1095 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or ∪ 𝐴) |
37 | | soss 4977 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑏‘𝑓) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑓))) |
38 | 35, 36, 37 | sylc 63 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐵 Or (𝑏‘𝑓)) |
39 | | simpll2 1094 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → 𝐴 ⊆ Fin) |
40 | 39, 31 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (𝑏‘𝑓) ∈ Fin) |
41 | | finnisoeu 8819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝐵 Or (𝑏‘𝑓) ∧ (𝑏‘𝑓) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
42 | 38, 40, 41 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
43 | | iotacl 5791 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}) |
44 | 42, 43 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))}) |
45 | | iotaex 5785 |
. . . . . . . . . . . . . . . . . . 19
⊢
(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ V |
46 | | isoeq1 6467 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))) |
47 | | isoeq1 6467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))) |
48 | 47 | cbvabv 2734 |
. . . . . . . . . . . . . . . . . . 19
⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} |
49 | 45, 46, 48 | elab2 3323 |
. . . . . . . . . . . . . . . . . 18
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
50 | 44, 49 | sylib 207 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) |
51 | | isof1o 6473 |
. . . . . . . . . . . . . . . . 17
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓)) |
52 | | f1of 6050 |
. . . . . . . . . . . . . . . . 17
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))–1-1-onto→(𝑏‘𝑓) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓)) |
53 | 50, 51, 52 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))):(card‘(𝑏‘𝑓))⟶(𝑏‘𝑓)) |
54 | 53 | ffvelrnda 6267 |
. . . . . . . . . . . . . . 15
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ (𝑏‘𝑓)) |
55 | 34, 54 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ 𝑔 ∈ (card‘(𝑏‘𝑓))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) ∈ ∪ 𝐴) |
56 | | simprl 790 |
. . . . . . . . . . . . . . 15
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → 𝑎 ∈ ∪ 𝐴) |
57 | 56 | ad2antrr 758 |
. . . . . . . . . . . . . 14
⊢
(((((𝐴 ≼
ω ∧ 𝐴 ⊆ Fin
∧ 𝐵 Or ∪ 𝐴)
∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) ∧ ¬ 𝑔 ∈ (card‘(𝑏‘𝑓))) → 𝑎 ∈ ∪ 𝐴) |
58 | 55, 57 | ifclda 4070 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑓 ∈ ω ∧ 𝑔 ∈ ω)) → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴) |
59 | 58 | ralrimivva 2954 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∀𝑓 ∈ ω ∀𝑔 ∈ ω if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴) |
60 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) = (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)) |
61 | 60 | fmpt2 7126 |
. . . . . . . . . . . 12
⊢
(∀𝑓 ∈
ω ∀𝑔 ∈
ω if(𝑔 ∈
(card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) ∈ ∪ 𝐴 ↔ (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴) |
62 | 59, 61 | sylib 207 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴) |
63 | | eluni 4375 |
. . . . . . . . . . . . 13
⊢ (𝑐 ∈ ∪ 𝐴
↔ ∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) |
64 | | simplrr 797 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑏:ω–onto→𝐴) |
65 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → 𝑖 ∈ 𝐴) |
66 | | foelrn 6286 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑏:ω–onto→𝐴 ∧ 𝑖 ∈ 𝐴) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗)) |
67 | 64, 65, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗)) |
68 | | simprrl 800 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑗 ∈ ω) |
69 | | ordom 6966 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ Ord
ω |
70 | | simpll2 1094 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐴 ⊆ Fin) |
71 | | simplrr 797 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω–onto→𝐴) |
72 | 71, 28 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑏:ω⟶𝐴) |
73 | 72, 68 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ 𝐴) |
74 | 70, 73 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ∈ Fin) |
75 | | ficardom 8670 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑏‘𝑗) ∈ Fin → (card‘(𝑏‘𝑗)) ∈ ω) |
76 | 74, 75 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ∈ ω) |
77 | | ordelss 5656 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((Ord
ω ∧ (card‘(𝑏‘𝑗)) ∈ ω) → (card‘(𝑏‘𝑗)) ⊆ ω) |
78 | 69, 76, 77 | sylancr 694 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (card‘(𝑏‘𝑗)) ⊆ ω) |
79 | | elssuni 4403 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ ((𝑏‘𝑗) ∈ 𝐴 → (𝑏‘𝑗) ⊆ ∪ 𝐴) |
80 | 73, 79 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑏‘𝑗) ⊆ ∪ 𝐴) |
81 | | simpll3 1095 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or ∪ 𝐴) |
82 | | soss 4977 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏‘𝑗) ⊆ ∪ 𝐴 → (𝐵 Or ∪ 𝐴 → 𝐵 Or (𝑏‘𝑗))) |
83 | 80, 81, 82 | sylc 63 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝐵 Or (𝑏‘𝑗)) |
84 | | finnisoeu 8819 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ ((𝐵 Or (𝑏‘𝑗) ∧ (𝑏‘𝑗) ∈ Fin) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
85 | 83, 74, 84 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
86 | | iotacl 5791 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(∃!ℎ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}) |
87 | 85, 86 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))}) |
88 | | iotaex 5785 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢
(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ V |
89 | | isoeq1 6467 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) → (𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
90 | | isoeq1 6467 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (ℎ = 𝑎 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) ↔ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
91 | 90 | cbvabv 2734 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} = {𝑎 ∣ 𝑎 Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} |
92 | 88, 89, 91 | elab2 3323 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) ∈ {ℎ ∣ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))} ↔ (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
93 | 87, 92 | sylib 207 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) |
94 | | isof1o 6473 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))) Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗)) |
95 | 93, 94 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗)) |
96 | | f1ocnv 6062 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗))) |
97 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)–1-1-onto→(card‘(𝑏‘𝑗)) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗))) |
98 | 95, 96, 97 | 3syl 18 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(𝑏‘𝑗)⟶(card‘(𝑏‘𝑗))) |
99 | | simprll 798 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ 𝑖) |
100 | | simprrr 801 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑖 = (𝑏‘𝑗)) |
101 | 99, 100 | eleqtrd 2690 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 ∈ (𝑏‘𝑗)) |
102 | 98, 101 | ffvelrnd 6268 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗))) |
103 | 78, 102 | sseldd 3569 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) |
104 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑗 → (𝑏‘𝑓) = (𝑏‘𝑗)) |
105 | 104 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑗 → (card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗))) |
106 | 105 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑗 → (𝑔 ∈ (card‘(𝑏‘𝑓)) ↔ 𝑔 ∈ (card‘(𝑏‘𝑗)))) |
107 | | isoeq4 6470 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢
((card‘(𝑏‘𝑓)) = (card‘(𝑏‘𝑗)) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)))) |
108 | 105, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)))) |
109 | | isoeq5 6471 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ ((𝑏‘𝑓) = (𝑏‘𝑗) → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
110 | 104, 109 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
111 | 108, 110 | bitrd 267 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑓 = 𝑗 → (ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)) ↔ ℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
112 | 111 | iotabidv 5789 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑓 = 𝑗 → (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓))) = (℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))) |
113 | 112 | fveq1d 6105 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑓 = 𝑗 → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔)) |
114 | 106, 113 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 = 𝑗 → if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎) = if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎)) |
115 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → (𝑔 ∈ (card‘(𝑏‘𝑗)) ↔ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)))) |
116 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
117 | 115, 116 | ifbieq1d 4059 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑔 = (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) → if(𝑔 ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑔), 𝑎) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
118 | | fvex 6113 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) ∈ V |
119 | | vex 3176 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝑎 ∈ V |
120 | 118, 119 | ifex 4106 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) ∈ V |
121 | 114, 117,
60, 120 | ovmpt2 6694 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑗 ∈ ω ∧ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
122 | 68, 103, 121 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎)) |
123 | 102 | iftrued 4044 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → if((◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ (card‘(𝑏‘𝑗)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)), 𝑎) = ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
124 | | f1ocnvfv2 6433 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗))):(card‘(𝑏‘𝑗))–1-1-onto→(𝑏‘𝑗) ∧ 𝑐 ∈ (𝑏‘𝑗)) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐) |
125 | 95, 101, 124 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐)) = 𝑐) |
126 | 122, 123,
125 | 3eqtrrd 2649 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) |
127 | | rspceov 6590 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑗 ∈ ω ∧ (◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐) ∈ ω ∧ 𝑐 = (𝑗(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))(◡(℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑗)), (𝑏‘𝑗)))‘𝑐))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
128 | 68, 103, 126, 127 | syl3anc 1318 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)))) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
129 | 128 | expr 641 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ((𝑗 ∈ ω ∧ 𝑖 = (𝑏‘𝑗)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
130 | 129 | expd 451 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (𝑗 ∈ ω → (𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)))) |
131 | 130 | rexlimdv 3012 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → (∃𝑗 ∈ ω 𝑖 = (𝑏‘𝑗) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
132 | 67, 131 | mpd 15 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) ∧ (𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴)) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
133 | 132 | ex 449 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ((𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
134 | 133 | exlimdv 1848 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (∃𝑖(𝑐 ∈ 𝑖 ∧ 𝑖 ∈ 𝐴) → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
135 | 63, 134 | syl5bi 231 |
. . . . . . . . . . . 12
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑐 ∈ ∪ 𝐴 → ∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
136 | 135 | ralrimiv 2948 |
. . . . . . . . . . 11
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∀𝑐 ∈ ∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒)) |
137 | | foov 6706 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 ↔ ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)⟶∪ 𝐴
∧ ∀𝑐 ∈
∪ 𝐴∃𝑑 ∈ ω ∃𝑒 ∈ ω 𝑐 = (𝑑(𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎))𝑒))) |
138 | 62, 136, 137 | sylanbrc 695 |
. . . . . . . . . 10
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → (𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴) |
139 | | fodomnum 8763 |
. . . . . . . . . 10
⊢ ((ω
× ω) ∈ dom card → ((𝑓 ∈ ω, 𝑔 ∈ ω ↦ if(𝑔 ∈ (card‘(𝑏‘𝑓)), ((℩ℎℎ Isom E , 𝐵 ((card‘(𝑏‘𝑓)), (𝑏‘𝑓)))‘𝑔), 𝑎)):(ω × ω)–onto→∪ 𝐴 → ∪ 𝐴
≼ (ω × ω))) |
140 | 26, 138, 139 | mpsyl 66 |
. . . . . . . . 9
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼ (ω ×
ω)) |
141 | | xpomen 8721 |
. . . . . . . . 9
⊢ (ω
× ω) ≈ ω |
142 | | domentr 7901 |
. . . . . . . . 9
⊢ ((∪ 𝐴
≼ (ω × ω) ∧ (ω × ω) ≈
ω) → ∪ 𝐴 ≼ ω) |
143 | 140, 141,
142 | sylancl 693 |
. . . . . . . 8
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ (𝑎 ∈ ∪ 𝐴
∧ 𝑏:ω–onto→𝐴)) → ∪ 𝐴 ≼
ω) |
144 | 143 | expr 641 |
. . . . . . 7
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼
ω)) |
145 | 144 | exlimdv 1848 |
. . . . . 6
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → (∃𝑏 𝑏:ω–onto→𝐴 → ∪ 𝐴 ≼
ω)) |
146 | 21, 145 | mpd 15 |
. . . . 5
⊢ (((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) ∧ 𝑎 ∈ ∪ 𝐴) → ∪ 𝐴
≼ ω) |
147 | 146 | expcom 450 |
. . . 4
⊢ (𝑎 ∈ ∪ 𝐴
→ ((𝐴 ≼ ω
∧ 𝐴 ⊆ Fin ∧
𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
148 | 147 | exlimiv 1845 |
. . 3
⊢
(∃𝑎 𝑎 ∈ ∪ 𝐴
→ ((𝐴 ≼ ω
∧ 𝐴 ⊆ Fin ∧
𝐵 Or ∪ 𝐴)
→ ∪ 𝐴 ≼ ω)) |
149 | 6, 148 | sylbi 206 |
. 2
⊢ (∪ 𝐴
≠ ∅ → ((𝐴
≼ ω ∧ 𝐴
⊆ Fin ∧ 𝐵 Or
∪ 𝐴) → ∪ 𝐴 ≼
ω)) |
150 | 5, 149 | pm2.61ine 2865 |
1
⊢ ((𝐴 ≼ ω ∧ 𝐴 ⊆ Fin ∧ 𝐵 Or ∪
𝐴) → ∪ 𝐴
≼ ω) |