This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem enfin2i

Description: II-finiteness is a cardinal property. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Assertion enfin2i ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinII → 𝐵 ∈ FinII ) )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
2 elpwi ⊢ ( 𝑥 ∈ 𝒫 𝒫 𝐵 → 𝑥 ⊆ 𝒫 𝐵 )
3 imauni ⊢ ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) = ∪ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ( 𝑓 “ 𝑧 )
4 vex ⊢ 𝑓 ∈ V
5 4 imaex ⊢ ( 𝑓 “ 𝑧 ) ∈ V
6 5 dfiun2 ⊢ ∪ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ( 𝑓 “ 𝑧 ) = ∪ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) }
7 3 6 eqtri ⊢ ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) = ∪ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) }
8 imaeq2 ⊢ ( 𝑦 = 𝑧 → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ 𝑧 ) )
9 8 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝑓 “ 𝑦 ) ∈ 𝑥 ↔ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) )
10 9 rexrab ⊢ ( ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) ↔ ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) )
11 eleq1 ⊢ ( 𝑤 = ( 𝑓 “ 𝑧 ) → ( 𝑤 ∈ 𝑥 ↔ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) )
12 11 biimparc ⊢ ( ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) → 𝑤 ∈ 𝑥 )
13 12 rexlimivw ⊢ ( ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) → 𝑤 ∈ 𝑥 )
14 cnvimass ⊢ ( ◡ 𝑓 “ 𝑤 ) ⊆ dom 𝑓
15 f1odm ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → dom 𝑓 = 𝐴 )
16 15 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → dom 𝑓 = 𝐴 )
17 14 16 sseqtrid ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ( ◡ 𝑓 “ 𝑤 ) ⊆ 𝐴 )
18 4 cnvex ⊢ ◡ 𝑓 ∈ V
19 18 imaex ⊢ ( ◡ 𝑓 “ 𝑤 ) ∈ V
20 19 elpw ⊢ ( ( ◡ 𝑓 “ 𝑤 ) ∈ 𝒫 𝐴 ↔ ( ◡ 𝑓 “ 𝑤 ) ⊆ 𝐴 )
21 17 20 sylibr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ( ◡ 𝑓 “ 𝑤 ) ∈ 𝒫 𝐴 )
22 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
23 22 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → 𝑓 : 𝐴 –onto→ 𝐵 )
24 simprl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → 𝑥 ⊆ 𝒫 𝐵 )
25 24 sselda ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 ∈ 𝒫 𝐵 )
26 25 elpwid ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 ⊆ 𝐵 )
27 foimacnv ⊢ ( ( 𝑓 : 𝐴 –onto→ 𝐵 ∧ 𝑤 ⊆ 𝐵 ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) = 𝑤 )
28 23 26 27 syl2anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) = 𝑤 )
29 28 eqcomd ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) )
30 simpr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → 𝑤 ∈ 𝑥 )
31 29 30 eqeltrrd ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 )
32 imaeq2 ⊢ ( 𝑧 = ( ◡ 𝑓 “ 𝑤 ) → ( 𝑓 “ 𝑧 ) = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) )
33 32 eleq1d ⊢ ( 𝑧 = ( ◡ 𝑓 “ 𝑤 ) → ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ↔ ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 ) )
34 32 eqeq2d ⊢ ( 𝑧 = ( ◡ 𝑓 “ 𝑤 ) → ( 𝑤 = ( 𝑓 “ 𝑧 ) ↔ 𝑤 = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ) )
35 33 34 anbi12d ⊢ ( 𝑧 = ( ◡ 𝑓 “ 𝑤 ) → ( ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) ↔ ( ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ) ) )
36 35 rspcev ⊢ ( ( ( ◡ 𝑓 “ 𝑤 ) ∈ 𝒫 𝐴 ∧ ( ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ) ) → ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) )
37 21 31 29 36 syl12anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) )
38 37 ex ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ( 𝑤 ∈ 𝑥 → ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) ) )
39 13 38 impbid2 ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ( ∃ 𝑧 ∈ 𝒫 𝐴 ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ 𝑤 = ( 𝑓 “ 𝑧 ) ) ↔ 𝑤 ∈ 𝑥 ) )
40 10 39 bitrid ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ( ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) ↔ 𝑤 ∈ 𝑥 ) )
41 40 eqabcdv ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) } = 𝑥 )
42 41 unieqd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∪ { 𝑤 ∣ ∃ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } 𝑤 = ( 𝑓 “ 𝑧 ) } = ∪ 𝑥 )
43 7 42 eqtrid ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) = ∪ 𝑥 )
44 simplr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → 𝐴 ∈ FinII )
45 ssrab2 ⊢ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ⊆ 𝒫 𝐴
46 45 a1i ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ⊆ 𝒫 𝐴 )
47 simprrl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → 𝑥 ≠ ∅ )
48 n0 ⊢ ( 𝑥 ≠ ∅ ↔ ∃ 𝑤 𝑤 ∈ 𝑥 )
49 47 48 sylib ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∃ 𝑤 𝑤 ∈ 𝑥 )
50 imaeq2 ⊢ ( 𝑦 = ( ◡ 𝑓 “ 𝑤 ) → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) )
51 50 eleq1d ⊢ ( 𝑦 = ( ◡ 𝑓 “ 𝑤 ) → ( ( 𝑓 “ 𝑦 ) ∈ 𝑥 ↔ ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 ) )
52 51 rspcev ⊢ ( ( ( ◡ 𝑓 “ 𝑤 ) ∈ 𝒫 𝐴 ∧ ( 𝑓 “ ( ◡ 𝑓 “ 𝑤 ) ) ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑓 “ 𝑦 ) ∈ 𝑥 )
53 21 31 52 syl2anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ 𝑤 ∈ 𝑥 ) → ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑓 “ 𝑦 ) ∈ 𝑥 )
54 49 53 exlimddv ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑓 “ 𝑦 ) ∈ 𝑥 )
55 rabn0 ⊢ ( { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ≠ ∅ ↔ ∃ 𝑦 ∈ 𝒫 𝐴 ( 𝑓 “ 𝑦 ) ∈ 𝑥 )
56 54 55 sylibr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ≠ ∅ )
57 9 elrab ⊢ ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ↔ ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) )
58 imaeq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ 𝑤 ) )
59 58 eleq1d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑓 “ 𝑦 ) ∈ 𝑥 ↔ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) )
60 59 elrab ⊢ ( 𝑤 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ↔ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) )
61 57 60 anbi12i ⊢ ( ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ↔ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) )
62 simprrr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → [⊊] Or 𝑥 )
63 62 adantr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → [⊊] Or 𝑥 )
64 simprlr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( 𝑓 “ 𝑧 ) ∈ 𝑥 )
65 simprrr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( 𝑓 “ 𝑤 ) ∈ 𝑥 )
66 sorpssi ⊢ ( ( [⊊] Or 𝑥 ∧ ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) → ( ( 𝑓 “ 𝑧 ) ⊆ ( 𝑓 “ 𝑤 ) ∨ ( 𝑓 “ 𝑤 ) ⊆ ( 𝑓 “ 𝑧 ) ) )
67 63 64 65 66 syl12anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( ( 𝑓 “ 𝑧 ) ⊆ ( 𝑓 “ 𝑤 ) ∨ ( 𝑓 “ 𝑤 ) ⊆ ( 𝑓 “ 𝑧 ) ) )
68 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –1-1→ 𝐵 )
69 68 ad3antrrr ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
70 simprll ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → 𝑧 ∈ 𝒫 𝐴 )
71 70 elpwid ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → 𝑧 ⊆ 𝐴 )
72 simprrl ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → 𝑤 ∈ 𝒫 𝐴 )
73 72 elpwid ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → 𝑤 ⊆ 𝐴 )
74 f1imass ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑧 ⊆ 𝐴 ∧ 𝑤 ⊆ 𝐴 ) ) → ( ( 𝑓 “ 𝑧 ) ⊆ ( 𝑓 “ 𝑤 ) ↔ 𝑧 ⊆ 𝑤 ) )
75 69 71 73 74 syl12anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( ( 𝑓 “ 𝑧 ) ⊆ ( 𝑓 “ 𝑤 ) ↔ 𝑧 ⊆ 𝑤 ) )
76 f1imass ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ ( 𝑤 ⊆ 𝐴 ∧ 𝑧 ⊆ 𝐴 ) ) → ( ( 𝑓 “ 𝑤 ) ⊆ ( 𝑓 “ 𝑧 ) ↔ 𝑤 ⊆ 𝑧 ) )
77 69 73 71 76 syl12anc ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( ( 𝑓 “ 𝑤 ) ⊆ ( 𝑓 “ 𝑧 ) ↔ 𝑤 ⊆ 𝑧 ) )
78 75 77 orbi12d ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( ( ( 𝑓 “ 𝑧 ) ⊆ ( 𝑓 “ 𝑤 ) ∨ ( 𝑓 “ 𝑤 ) ⊆ ( 𝑓 “ 𝑧 ) ) ↔ ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) ) )
79 67 78 mpbid ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( ( 𝑧 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑧 ) ∈ 𝑥 ) ∧ ( 𝑤 ∈ 𝒫 𝐴 ∧ ( 𝑓 “ 𝑤 ) ∈ 𝑥 ) ) ) → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) )
80 61 79 sylan2b ⊢ ( ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) ∧ ( 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∧ 𝑤 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ) → ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) )
81 80 ralrimivva ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∀ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∀ 𝑤 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) )
82 sorpss ⊢ ( [⊊] Or { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ↔ ∀ 𝑧 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∀ 𝑤 ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ( 𝑧 ⊆ 𝑤 ∨ 𝑤 ⊆ 𝑧 ) )
83 81 82 sylibr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → [⊊] Or { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } )
84 fin2i ⊢ ( ( ( 𝐴 ∈ FinII ∧ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ⊆ 𝒫 𝐴 ) ∧ ( { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ≠ ∅ ∧ [⊊] Or { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ) → ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } )
85 44 46 56 83 84 syl22anc ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } )
86 imaeq2 ⊢ ( 𝑧 = ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } → ( 𝑓 “ 𝑧 ) = ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) )
87 86 eleq1d ⊢ ( 𝑧 = ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } → ( ( 𝑓 “ 𝑧 ) ∈ 𝑥 ↔ ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ∈ 𝑥 ) )
88 9 cbvrabv ⊢ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } = { 𝑧 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑧 ) ∈ 𝑥 }
89 87 88 elrab2 ⊢ ( ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ↔ ( ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∈ 𝒫 𝐴 ∧ ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ∈ 𝑥 ) )
90 89 simprbi ⊢ ( ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ∈ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } → ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ∈ 𝑥 )
91 85 90 syl ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ( 𝑓 “ ∪ { 𝑦 ∈ 𝒫 𝐴 ∣ ( 𝑓 “ 𝑦 ) ∈ 𝑥 } ) ∈ 𝑥 )
92 43 91 eqeltrrd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ ( 𝑥 ⊆ 𝒫 𝐵 ∧ ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) ) ) → ∪ 𝑥 ∈ 𝑥 )
93 92 expr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ 𝑥 ⊆ 𝒫 𝐵 ) → ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
94 2 93 sylan2 ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) ∧ 𝑥 ∈ 𝒫 𝒫 𝐵 ) → ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
95 94 ralrimiva ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝐴 ∈ FinII ) → ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) )
96 95 ex ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ FinII → ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
97 96 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝐴 ∈ FinII → ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
98 1 97 sylbi ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinII → ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
99 relen ⊢ Rel ≈
100 99 brrelex2i ⊢ ( 𝐴 ≈ 𝐵 → 𝐵 ∈ V )
101 isfin2 ⊢ ( 𝐵 ∈ V → ( 𝐵 ∈ FinII ↔ ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
102 100 101 syl ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐵 ∈ FinII ↔ ∀ 𝑥 ∈ 𝒫 𝒫 𝐵 ( ( 𝑥 ≠ ∅ ∧ [⊊] Or 𝑥 ) → ∪ 𝑥 ∈ 𝑥 ) ) )
103 98 102 sylibrd ⊢ ( 𝐴 ≈ 𝐵 → ( 𝐴 ∈ FinII → 𝐵 ∈ FinII ) )