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 ) ≈ 𝐴 )