Step | Hyp | Ref
| Expression |
1 | | infxpidm2 8723 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝐴 × 𝐴) ≈ 𝐴) |
2 | | infn0 8107 |
. . . . . . . 8
⊢ (ω
≼ 𝐴 → 𝐴 ≠ ∅) |
3 | 2 | adantl 481 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → 𝐴 ≠ ∅) |
4 | | fseqen 8733 |
. . . . . . 7
⊢ (((𝐴 × 𝐴) ≈ 𝐴 ∧ 𝐴 ≠ ∅) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≈ (ω × 𝐴)) |
5 | 1, 3, 4 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≈ (ω × 𝐴)) |
6 | | xpdom1g 7942 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (ω
× 𝐴) ≼ (𝐴 × 𝐴)) |
7 | | domentr 7901 |
. . . . . . 7
⊢
(((ω × 𝐴) ≼ (𝐴 × 𝐴) ∧ (𝐴 × 𝐴) ≈ 𝐴) → (ω × 𝐴) ≼ 𝐴) |
8 | 6, 1, 7 | syl2anc 691 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (ω
× 𝐴) ≼ 𝐴) |
9 | | endomtr 7900 |
. . . . . 6
⊢
((∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≈ (ω × 𝐴) ∧ (ω × 𝐴) ≼ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ≼ 𝐴) |
10 | 5, 8, 9 | syl2anc 691 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≼ 𝐴) |
11 | | numdom 8744 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≼ 𝐴) → ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∈ dom
card) |
12 | 10, 11 | syldan 486 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ dom
card) |
13 | | eliun 4460 |
. . . . . . . . 9
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↔ ∃𝑛 ∈ ω 𝑥 ∈ (𝐴 ↑𝑚 𝑛)) |
14 | | elmapi 7765 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (𝐴 ↑𝑚 𝑛) → 𝑥:𝑛⟶𝐴) |
15 | 14 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → 𝑥:𝑛⟶𝐴) |
16 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝑥:𝑛⟶𝐴 → ran 𝑥 ⊆ 𝐴) |
17 | 15, 16 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → ran 𝑥 ⊆ 𝐴) |
18 | | vex 3176 |
. . . . . . . . . . . . . . 15
⊢ 𝑥 ∈ V |
19 | 18 | rnex 6992 |
. . . . . . . . . . . . . 14
⊢ ran 𝑥 ∈ V |
20 | 19 | elpw 4114 |
. . . . . . . . . . . . 13
⊢ (ran
𝑥 ∈ 𝒫 𝐴 ↔ ran 𝑥 ⊆ 𝐴) |
21 | 17, 20 | sylibr 223 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → ran 𝑥 ∈ 𝒫 𝐴) |
22 | | simprl 790 |
. . . . . . . . . . . . . 14
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → 𝑛 ∈ ω) |
23 | | ssid 3587 |
. . . . . . . . . . . . . 14
⊢ 𝑛 ⊆ 𝑛 |
24 | | ssnnfi 8064 |
. . . . . . . . . . . . . 14
⊢ ((𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑛) → 𝑛 ∈ Fin) |
25 | 22, 23, 24 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → 𝑛 ∈ Fin) |
26 | | ffn 5958 |
. . . . . . . . . . . . . . 15
⊢ (𝑥:𝑛⟶𝐴 → 𝑥 Fn 𝑛) |
27 | | dffn4 6034 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 Fn 𝑛 ↔ 𝑥:𝑛–onto→ran 𝑥) |
28 | 26, 27 | sylib 207 |
. . . . . . . . . . . . . 14
⊢ (𝑥:𝑛⟶𝐴 → 𝑥:𝑛–onto→ran 𝑥) |
29 | 15, 28 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → 𝑥:𝑛–onto→ran 𝑥) |
30 | | fofi 8135 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ Fin ∧ 𝑥:𝑛–onto→ran 𝑥) → ran 𝑥 ∈ Fin) |
31 | 25, 29, 30 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → ran 𝑥 ∈ Fin) |
32 | 21, 31 | elind 3760 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ (𝑛 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑛))) → ran 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
33 | 32 | expr 641 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑛 ∈ ω) → (𝑥 ∈ (𝐴 ↑𝑚 𝑛) → ran 𝑥 ∈ (𝒫 𝐴 ∩ Fin))) |
34 | 33 | rexlimdva 3013 |
. . . . . . . . 9
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(∃𝑛 ∈ ω
𝑥 ∈ (𝐴 ↑𝑚 𝑛) → ran 𝑥 ∈ (𝒫 𝐴 ∩ Fin))) |
35 | 13, 34 | syl5bi 231 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) → ran 𝑥 ∈ (𝒫 𝐴 ∩ Fin))) |
36 | 35 | imp 444 |
. . . . . . 7
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) → ran 𝑥 ∈ (𝒫 𝐴 ∩ Fin)) |
37 | | eqid 2610 |
. . . . . . 7
⊢ (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) = (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) |
38 | 36, 37 | fmptd 6292 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)⟶(𝒫 𝐴 ∩ Fin)) |
39 | | ffn 5958 |
. . . . . 6
⊢ ((𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)⟶(𝒫 𝐴 ∩ Fin) → (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) Fn ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) Fn ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
41 | | frn 5966 |
. . . . . . 7
⊢ ((𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)⟶(𝒫 𝐴 ∩ Fin) → ran (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) ⊆ (𝒫 𝐴 ∩ Fin)) |
42 | 38, 41 | syl 17 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → ran
(𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) ⊆ (𝒫 𝐴 ∩ Fin)) |
43 | | inss2 3796 |
. . . . . . . . . . . 12
⊢
(𝒫 𝐴 ∩
Fin) ⊆ Fin |
44 | | simpr 476 |
. . . . . . . . . . . 12
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
45 | 43, 44 | sseldi 3566 |
. . . . . . . . . . 11
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → 𝑦 ∈ Fin) |
46 | | isfi 7865 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ Fin ↔ ∃𝑚 ∈ ω 𝑦 ≈ 𝑚) |
47 | 45, 46 | sylib 207 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑚 ∈ ω 𝑦 ≈ 𝑚) |
48 | | ensym 7891 |
. . . . . . . . . . . . 13
⊢ (𝑦 ≈ 𝑚 → 𝑚 ≈ 𝑦) |
49 | | bren 7850 |
. . . . . . . . . . . . 13
⊢ (𝑚 ≈ 𝑦 ↔ ∃𝑥 𝑥:𝑚–1-1-onto→𝑦) |
50 | 48, 49 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝑦 ≈ 𝑚 → ∃𝑥 𝑥:𝑚–1-1-onto→𝑦) |
51 | | simprl 790 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑚 ∈ ω) |
52 | | f1of 6050 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥:𝑚–1-1-onto→𝑦 → 𝑥:𝑚⟶𝑦) |
53 | 52 | ad2antll 761 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑥:𝑚⟶𝑦) |
54 | | inss1 3795 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(𝒫 𝐴 ∩
Fin) ⊆ 𝒫 𝐴 |
55 | | simplr 788 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) |
56 | 54, 55 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑦 ∈ 𝒫 𝐴) |
57 | 56 | elpwid 4118 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑦 ⊆ 𝐴) |
58 | 53, 57 | fssd 5970 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑥:𝑚⟶𝐴) |
59 | | simplll 794 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝐴 ∈ dom card) |
60 | | vex 3176 |
. . . . . . . . . . . . . . . . . . 19
⊢ 𝑚 ∈ V |
61 | | elmapg 7757 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐴 ∈ dom card ∧ 𝑚 ∈ V) → (𝑥 ∈ (𝐴 ↑𝑚 𝑚) ↔ 𝑥:𝑚⟶𝐴)) |
62 | 59, 60, 61 | sylancl 693 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → (𝑥 ∈ (𝐴 ↑𝑚 𝑚) ↔ 𝑥:𝑚⟶𝐴)) |
63 | 58, 62 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑥 ∈ (𝐴 ↑𝑚 𝑚)) |
64 | | oveq2 6557 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝐴 ↑𝑚 𝑛) = (𝐴 ↑𝑚 𝑚)) |
65 | 64 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (𝑥 ∈ (𝐴 ↑𝑚 𝑛) ↔ 𝑥 ∈ (𝐴 ↑𝑚 𝑚))) |
66 | 65 | rspcev 3282 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑚 ∈ ω ∧ 𝑥 ∈ (𝐴 ↑𝑚 𝑚)) → ∃𝑛 ∈ ω 𝑥 ∈ (𝐴 ↑𝑚 𝑛)) |
67 | 51, 63, 66 | syl2anc 691 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → ∃𝑛 ∈ ω 𝑥 ∈ (𝐴 ↑𝑚 𝑛)) |
68 | 67, 13 | sylibr 223 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)) |
69 | | f1ofo 6057 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥:𝑚–1-1-onto→𝑦 → 𝑥:𝑚–onto→𝑦) |
70 | 69 | ad2antll 761 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑥:𝑚–onto→𝑦) |
71 | | forn 6031 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥:𝑚–onto→𝑦 → ran 𝑥 = 𝑦) |
72 | 70, 71 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → ran 𝑥 = 𝑦) |
73 | 72 | eqcomd 2616 |
. . . . . . . . . . . . . . 15
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → 𝑦 = ran 𝑥) |
74 | 68, 73 | jca 553 |
. . . . . . . . . . . . . 14
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ (𝑚 ∈ ω ∧ 𝑥:𝑚–1-1-onto→𝑦)) → (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥)) |
75 | 74 | expr 641 |
. . . . . . . . . . . . 13
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑚 ∈ ω) → (𝑥:𝑚–1-1-onto→𝑦 → (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥))) |
76 | 75 | eximdv 1833 |
. . . . . . . . . . . 12
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑚 ∈ ω) →
(∃𝑥 𝑥:𝑚–1-1-onto→𝑦 → ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥))) |
77 | 50, 76 | syl5 33 |
. . . . . . . . . . 11
⊢ ((((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) ∧ 𝑚 ∈ ω) → (𝑦 ≈ 𝑚 → ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥))) |
78 | 77 | rexlimdva 3013 |
. . . . . . . . . 10
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) →
(∃𝑚 ∈ ω
𝑦 ≈ 𝑚 → ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥))) |
79 | 47, 78 | mpd 15 |
. . . . . . . . 9
⊢ (((𝐴 ∈ dom card ∧ ω
≼ 𝐴) ∧ 𝑦 ∈ (𝒫 𝐴 ∩ Fin)) → ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥)) |
80 | 79 | ex 449 |
. . . . . . . 8
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥))) |
81 | | vex 3176 |
. . . . . . . . . 10
⊢ 𝑦 ∈ V |
82 | 37 | elrnmpt 5293 |
. . . . . . . . . 10
⊢ (𝑦 ∈ V → (𝑦 ∈ ran (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) ↔ ∃𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)𝑦 = ran 𝑥)) |
83 | 81, 82 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑦 ∈ ran (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) ↔ ∃𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)𝑦 = ran 𝑥) |
84 | | df-rex 2902 |
. . . . . . . . 9
⊢
(∃𝑥 ∈
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)𝑦 = ran 𝑥 ↔ ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥)) |
85 | 83, 84 | bitri 263 |
. . . . . . . 8
⊢ (𝑦 ∈ ran (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) ↔ ∃𝑥(𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ∧ 𝑦 = ran 𝑥)) |
86 | 80, 85 | syl6ibr 241 |
. . . . . . 7
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑦 ∈ (𝒫 𝐴 ∩ Fin) → 𝑦 ∈ ran (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥))) |
87 | 86 | ssrdv 3574 |
. . . . . 6
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(𝒫 𝐴 ∩ Fin)
⊆ ran (𝑥 ∈
∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥)) |
88 | 42, 87 | eqssd 3585 |
. . . . 5
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → ran
(𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥) = (𝒫 𝐴 ∩ Fin)) |
89 | | df-fo 5810 |
. . . . 5
⊢ ((𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)–onto→(𝒫 𝐴 ∩ Fin) ↔ ((𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) Fn ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∧ ran (𝑥 ∈ ∪
𝑛 ∈ ω (𝐴 ↑𝑚
𝑛) ↦ ran 𝑥) = (𝒫 𝐴 ∩ Fin))) |
90 | 40, 88, 89 | sylanbrc 695 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → (𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)–onto→(𝒫 𝐴 ∩ Fin)) |
91 | | fodomnum 8763 |
. . . 4
⊢ (∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∈ dom card → ((𝑥 ∈ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ↦ ran 𝑥):∪ 𝑛 ∈ ω (𝐴 ↑𝑚
𝑛)–onto→(𝒫 𝐴 ∩ Fin) → (𝒫 𝐴 ∩ Fin) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛))) |
92 | 12, 90, 91 | sylc 63 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(𝒫 𝐴 ∩ Fin)
≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛)) |
93 | | domtr 7895 |
. . 3
⊢
(((𝒫 𝐴 ∩
Fin) ≼ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ∧ ∪ 𝑛 ∈ ω (𝐴 ↑𝑚 𝑛) ≼ 𝐴) → (𝒫 𝐴 ∩ Fin) ≼ 𝐴) |
94 | 92, 10, 93 | syl2anc 691 |
. 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(𝒫 𝐴 ∩ Fin)
≼ 𝐴) |
95 | | pwexg 4776 |
. . . . 5
⊢ (𝐴 ∈ dom card →
𝒫 𝐴 ∈
V) |
96 | 95 | adantr 480 |
. . . 4
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → 𝒫
𝐴 ∈
V) |
97 | | inex1g 4729 |
. . . 4
⊢
(𝒫 𝐴 ∈
V → (𝒫 𝐴 ∩
Fin) ∈ V) |
98 | 96, 97 | syl 17 |
. . 3
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(𝒫 𝐴 ∩ Fin)
∈ V) |
99 | | infpwfidom 8734 |
. . 3
⊢
((𝒫 𝐴 ∩
Fin) ∈ V → 𝐴
≼ (𝒫 𝐴 ∩
Fin)) |
100 | 98, 99 | syl 17 |
. 2
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) → 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) |
101 | | sbth 7965 |
. 2
⊢
(((𝒫 𝐴 ∩
Fin) ≼ 𝐴 ∧ 𝐴 ≼ (𝒫 𝐴 ∩ Fin)) → (𝒫
𝐴 ∩ Fin) ≈ 𝐴) |
102 | 94, 100, 101 | syl2anc 691 |
1
⊢ ((𝐴 ∈ dom card ∧ ω
≼ 𝐴) →
(𝒫 𝐴 ∩ Fin)
≈ 𝐴) |