Metamath Proof Explorer

Theorem infpwfien

Description: Any infinite well-orderable set is equinumerous to its set of finite subsets. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion infpwfien ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 )

Proof

Step Hyp Ref Expression
1 infxpidm2 ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝐴 × 𝐴 ) ≈ 𝐴 )
2 infn0 ⊢ ( ω ≼ 𝐴 → 𝐴 ≠ ∅ )
3 2 adantl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ≠ ∅ )
4 fseqen ⊢ ( ( ( 𝐴 × 𝐴 ) ≈ 𝐴 ∧ 𝐴 ≠ ∅ ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
5 1 3 4 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) )
6 xpdom1g ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ω × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) )
7 domentr ⊢ ( ( ( ω × 𝐴 ) ≼ ( 𝐴 × 𝐴 ) ∧ ( 𝐴 × 𝐴 ) ≈ 𝐴 ) → ( ω × 𝐴 ) ≼ 𝐴 )
8 6 1 7 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ω × 𝐴 ) ≼ 𝐴 )
9 endomtr ⊢ ( ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≈ ( ω × 𝐴 ) ∧ ( ω × 𝐴 ) ≼ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ 𝐴 )
10 5 8 9 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ 𝐴 )
11 numdom ⊢ ( ( 𝐴 ∈ dom card ∧ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ dom card )
12 10 11 syldan ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ dom card )
13 eliun ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↔ ∃ 𝑛 ∈ ω 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) )
14 elmapi ⊢ ( 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) → 𝑥 : 𝑛 ⟶ 𝐴 )
15 14 ad2antll ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑥 : 𝑛 ⟶ 𝐴 )
16 15 frnd ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ran 𝑥 ⊆ 𝐴 )
17 vex ⊢ 𝑥 ∈ V
18 17 rnex ⊢ ran 𝑥 ∈ V
19 18 elpw ⊢ ( ran 𝑥 ∈ 𝒫 𝐴 ↔ ran 𝑥 ⊆ 𝐴 )
20 16 19 sylibr ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ran 𝑥 ∈ 𝒫 𝐴 )
21 simprl ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑛 ∈ ω )
22 ssid ⊢ 𝑛 ⊆ 𝑛
23 ssnnfi ⊢ ( ( 𝑛 ∈ ω ∧ 𝑛 ⊆ 𝑛 ) → 𝑛 ∈ Fin )
24 21 22 23 sylancl ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑛 ∈ Fin )
25 ffn ⊢ ( 𝑥 : 𝑛 ⟶ 𝐴 → 𝑥 Fn 𝑛 )
26 dffn4 ⊢ ( 𝑥 Fn 𝑛 ↔ 𝑥 : 𝑛 –onto→ ran 𝑥 )
27 25 26 sylib ⊢ ( 𝑥 : 𝑛 ⟶ 𝐴 → 𝑥 : 𝑛 –onto→ ran 𝑥 )
28 15 27 syl ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → 𝑥 : 𝑛 –onto→ ran 𝑥 )
29 fofi ⊢ ( ( 𝑛 ∈ Fin ∧ 𝑥 : 𝑛 –onto→ ran 𝑥 ) → ran 𝑥 ∈ Fin )
30 24 28 29 syl2anc ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ran 𝑥 ∈ Fin )
31 20 30 elind ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ ( 𝑛 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ) ) → ran 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
32 31 expr ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑛 ∈ ω ) → ( 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) → ran 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) )
33 32 rexlimdva ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( ∃ 𝑛 ∈ ω 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) → ran 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) )
34 13 33 syl5bi ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) → ran 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) ) )
35 34 imp ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) → ran 𝑥 ∈ ( 𝒫 𝐴 ∩ Fin ) )
36 35 fmpttd ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ⟶ ( 𝒫 𝐴 ∩ Fin ) )
37 36 ffnd ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) Fn ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
38 36 frnd ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) ⊆ ( 𝒫 𝐴 ∩ Fin ) )
39 simpr ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
40 39 elin2d ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → 𝑦 ∈ Fin )
41 isfi ⊢ ( 𝑦 ∈ Fin ↔ ∃ 𝑚 ∈ ω 𝑦 ≈ 𝑚 )
42 40 41 sylib ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑚 ∈ ω 𝑦 ≈ 𝑚 )
43 ensym ⊢ ( 𝑦 ≈ 𝑚 → 𝑚 ≈ 𝑦 )
44 bren ⊢ ( 𝑚 ≈ 𝑦 ↔ ∃ 𝑥 𝑥 : 𝑚 –1-1-onto→ 𝑦 )
45 43 44 sylib ⊢ ( 𝑦 ≈ 𝑚 → ∃ 𝑥 𝑥 : 𝑚 –1-1-onto→ 𝑦 )
46 simprl ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑚 ∈ ω )
47 f1of ⊢ ( 𝑥 : 𝑚 –1-1-onto→ 𝑦 → 𝑥 : 𝑚 ⟶ 𝑦 )
48 47 ad2antll ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑥 : 𝑚 ⟶ 𝑦 )
49 simplr ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) )
50 49 elin1d ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑦 ∈ 𝒫 𝐴 )
51 50 elpwid ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑦 ⊆ 𝐴 )
52 48 51 fssd ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑥 : 𝑚 ⟶ 𝐴 )
53 simplll ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝐴 ∈ dom card )
54 vex ⊢ 𝑚 ∈ V
55 elmapg ⊢ ( ( 𝐴 ∈ dom card ∧ 𝑚 ∈ V ) → ( 𝑥 ∈ ( 𝐴 ↑m 𝑚 ) ↔ 𝑥 : 𝑚 ⟶ 𝐴 ) )
56 53 54 55 sylancl ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → ( 𝑥 ∈ ( 𝐴 ↑m 𝑚 ) ↔ 𝑥 : 𝑚 ⟶ 𝐴 ) )
57 52 56 mpbird ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑥 ∈ ( 𝐴 ↑m 𝑚 ) )
58 oveq2 ⊢ ( 𝑛 = 𝑚 → ( 𝐴 ↑m 𝑛 ) = ( 𝐴 ↑m 𝑚 ) )
59 58 eleq2d ⊢ ( 𝑛 = 𝑚 → ( 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) ↔ 𝑥 ∈ ( 𝐴 ↑m 𝑚 ) ) )
60 59 rspcev ⊢ ( ( 𝑚 ∈ ω ∧ 𝑥 ∈ ( 𝐴 ↑m 𝑚 ) ) → ∃ 𝑛 ∈ ω 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) )
61 46 57 60 syl2anc ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → ∃ 𝑛 ∈ ω 𝑥 ∈ ( 𝐴 ↑m 𝑛 ) )
62 61 13 sylibr ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
63 f1ofo ⊢ ( 𝑥 : 𝑚 –1-1-onto→ 𝑦 → 𝑥 : 𝑚 –onto→ 𝑦 )
64 63 ad2antll ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑥 : 𝑚 –onto→ 𝑦 )
65 forn ⊢ ( 𝑥 : 𝑚 –onto→ 𝑦 → ran 𝑥 = 𝑦 )
66 64 65 syl ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → ran 𝑥 = 𝑦 )
67 66 eqcomd ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → 𝑦 = ran 𝑥 )
68 62 67 jca ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ ( 𝑚 ∈ ω ∧ 𝑥 : 𝑚 –1-1-onto→ 𝑦 ) ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) )
69 68 expr ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑚 ∈ ω ) → ( 𝑥 : 𝑚 –1-1-onto→ 𝑦 → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) ) )
70 69 eximdv ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑚 ∈ ω ) → ( ∃ 𝑥 𝑥 : 𝑚 –1-1-onto→ 𝑦 → ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) ) )
71 45 70 syl5 ⊢ ( ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) ∧ 𝑚 ∈ ω ) → ( 𝑦 ≈ 𝑚 → ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) ) )
72 71 rexlimdva ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ( ∃ 𝑚 ∈ ω 𝑦 ≈ 𝑚 → ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) ) )
73 42 72 mpd ⊢ ( ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) ) → ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) )
74 73 ex ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) ) )
75 eqid ⊢ ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) = ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 )
76 75 elrnmpt ⊢ ( 𝑦 ∈ V → ( 𝑦 ∈ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) ↔ ∃ 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) 𝑦 = ran 𝑥 ) )
77 76 elv ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) ↔ ∃ 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) 𝑦 = ran 𝑥 )
78 df-rex ⊢ ( ∃ 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) 𝑦 = ran 𝑥 ↔ ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) )
79 77 78 bitri ⊢ ( 𝑦 ∈ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) ↔ ∃ 𝑥 ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ 𝑦 = ran 𝑥 ) )
80 74 79 syl6ibr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ Fin ) → 𝑦 ∈ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) ) )
81 80 ssrdv ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ⊆ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) )
82 38 81 eqssd ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) = ( 𝒫 𝐴 ∩ Fin ) )
83 df-fo ⊢ ( ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) –onto→ ( 𝒫 𝐴 ∩ Fin ) ↔ ( ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) Fn ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ran ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) = ( 𝒫 𝐴 ∩ Fin ) ) )
84 37 82 83 sylanbrc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) –onto→ ( 𝒫 𝐴 ∩ Fin ) )
85 fodomnum ⊢ ( ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∈ dom card → ( ( 𝑥 ∈ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ↦ ran 𝑥 ) : ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) –onto→ ( 𝒫 𝐴 ∩ Fin ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ) )
86 12 84 85 sylc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) )
87 domtr ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ≼ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ∧ ∪ 𝑛 ∈ ω ( 𝐴 ↑m 𝑛 ) ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≼ 𝐴 )
88 86 10 87 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≼ 𝐴 )
89 pwexg ⊢ ( 𝐴 ∈ dom card → 𝒫 𝐴 ∈ V )
90 89 adantr ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝒫 𝐴 ∈ V )
91 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
92 90 91 syl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ∈ V )
93 infpwfidom ⊢ ( ( 𝒫 𝐴 ∩ Fin ) ∈ V → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )
94 92 93 syl ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) )
95 sbth ⊢ ( ( ( 𝒫 𝐴 ∩ Fin ) ≼ 𝐴 ∧ 𝐴 ≼ ( 𝒫 𝐴 ∩ Fin ) ) → ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 )
96 88 94 95 syl2anc ⊢ ( ( 𝐴 ∈ dom card ∧ ω ≼ 𝐴 ) → ( 𝒫 𝐴 ∩ Fin ) ≈ 𝐴 )