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

Metamath Proof Explorer

Theorem ssenen

Description: Equinumerosity of equinumerous subsets of a set. (Contributed by NM, 30-Sep-2004) (Revised by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion ssenen ( 𝐴 ≈ 𝐵 → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶 ) } )

Proof

Step Hyp Ref Expression
1 bren ⊢ ( 𝐴 ≈ 𝐵 ↔ ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 )
2 f1odm ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → dom 𝑓 = 𝐴 )
3 vex ⊢ 𝑓 ∈ V
4 3 dmex ⊢ dom 𝑓 ∈ V
5 2 4 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐴 ∈ V )
6 pwexg ⊢ ( 𝐴 ∈ V → 𝒫 𝐴 ∈ V )
7 inex1g ⊢ ( 𝒫 𝐴 ∈ V → ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∈ V )
8 5 6 7 3syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∈ V )
9 f1ofo ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –onto→ 𝐵 )
10 forn ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ran 𝑓 = 𝐵 )
11 9 10 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ran 𝑓 = 𝐵 )
12 3 rnex ⊢ ran 𝑓 ∈ V
13 11 12 eqeltrrdi ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝐵 ∈ V )
14 pwexg ⊢ ( 𝐵 ∈ V → 𝒫 𝐵 ∈ V )
15 inex1g ⊢ ( 𝒫 𝐵 ∈ V → ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∈ V )
16 13 14 15 3syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∈ V )
17 f1of1 ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → 𝑓 : 𝐴 –1-1→ 𝐵 )
18 17 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → 𝑓 : 𝐴 –1-1→ 𝐵 )
19 13 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → 𝐵 ∈ V )
20 simpr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ⊆ 𝐴 )
21 vex ⊢ 𝑦 ∈ V
22 21 a1i ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → 𝑦 ∈ V )
23 f1imaen2g ⊢ ( ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝐵 ∈ V ) ∧ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ∈ V ) ) → ( 𝑓 “ 𝑦 ) ≈ 𝑦 )
24 18 19 20 22 23 syl22anc ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑓 “ 𝑦 ) ≈ 𝑦 )
25 entr ⊢ ( ( ( 𝑓 “ 𝑦 ) ≈ 𝑦 ∧ 𝑦 ≈ 𝐶 ) → ( 𝑓 “ 𝑦 ) ≈ 𝐶 )
26 24 25 sylan ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑦 ≈ 𝐶 ) → ( 𝑓 “ 𝑦 ) ≈ 𝐶 )
27 26 expl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶 ) → ( 𝑓 “ 𝑦 ) ≈ 𝐶 ) )
28 imassrn ⊢ ( 𝑓 “ 𝑦 ) ⊆ ran 𝑓
29 28 10 sseqtrid ⊢ ( 𝑓 : 𝐴 –onto→ 𝐵 → ( 𝑓 “ 𝑦 ) ⊆ 𝐵 )
30 9 29 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑓 “ 𝑦 ) ⊆ 𝐵 )
31 27 30 jctild ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶 ) → ( ( 𝑓 “ 𝑦 ) ⊆ 𝐵 ∧ ( 𝑓 “ 𝑦 ) ≈ 𝐶 ) ) )
32 elin ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
33 21 elpw ⊢ ( 𝑦 ∈ 𝒫 𝐴 ↔ 𝑦 ⊆ 𝐴 )
34 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≈ 𝐶 ↔ 𝑦 ≈ 𝐶 ) )
35 21 34 elab ⊢ ( 𝑦 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ↔ 𝑦 ≈ 𝐶 )
36 33 35 anbi12i ⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶 ) )
37 32 36 bitri ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑦 ⊆ 𝐴 ∧ 𝑦 ≈ 𝐶 ) )
38 elin ⊢ ( ( 𝑓 “ 𝑦 ) ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( 𝑓 “ 𝑦 ) ∈ 𝒫 𝐵 ∧ ( 𝑓 “ 𝑦 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
39 3 imaex ⊢ ( 𝑓 “ 𝑦 ) ∈ V
40 39 elpw ⊢ ( ( 𝑓 “ 𝑦 ) ∈ 𝒫 𝐵 ↔ ( 𝑓 “ 𝑦 ) ⊆ 𝐵 )
41 breq1 ⊢ ( 𝑥 = ( 𝑓 “ 𝑦 ) → ( 𝑥 ≈ 𝐶 ↔ ( 𝑓 “ 𝑦 ) ≈ 𝐶 ) )
42 39 41 elab ⊢ ( ( 𝑓 “ 𝑦 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ↔ ( 𝑓 “ 𝑦 ) ≈ 𝐶 )
43 40 42 anbi12i ⊢ ( ( ( 𝑓 “ 𝑦 ) ∈ 𝒫 𝐵 ∧ ( 𝑓 “ 𝑦 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( 𝑓 “ 𝑦 ) ⊆ 𝐵 ∧ ( 𝑓 “ 𝑦 ) ≈ 𝐶 ) )
44 38 43 bitri ⊢ ( ( 𝑓 “ 𝑦 ) ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( 𝑓 “ 𝑦 ) ⊆ 𝐵 ∧ ( 𝑓 “ 𝑦 ) ≈ 𝐶 ) )
45 31 37 44 3imtr4g ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → ( 𝑓 “ 𝑦 ) ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) )
46 f1ocnv ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 )
47 f1of1 ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐵 –1-1→ 𝐴 )
48 f1f1orn ⊢ ( ◡ 𝑓 : 𝐵 –1-1→ 𝐴 → ◡ 𝑓 : 𝐵 –1-1-onto→ ran ◡ 𝑓 )
49 f1of1 ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ ran ◡ 𝑓 → ◡ 𝑓 : 𝐵 –1-1→ ran ◡ 𝑓 )
50 47 48 49 3syl ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐵 –1-1→ ran ◡ 𝑓 )
51 vex ⊢ 𝑧 ∈ V
52 51 f1imaen ⊢ ( ( ◡ 𝑓 : 𝐵 –1-1→ ran ◡ 𝑓 ∧ 𝑧 ⊆ 𝐵 ) → ( ◡ 𝑓 “ 𝑧 ) ≈ 𝑧 )
53 50 52 sylan ⊢ ( ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑧 ⊆ 𝐵 ) → ( ◡ 𝑓 “ 𝑧 ) ≈ 𝑧 )
54 entr ⊢ ( ( ( ◡ 𝑓 “ 𝑧 ) ≈ 𝑧 ∧ 𝑧 ≈ 𝐶 ) → ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 )
55 53 54 sylan ⊢ ( ( ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑧 ≈ 𝐶 ) → ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 )
56 55 expl ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶 ) → ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) )
57 f1ofo ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ◡ 𝑓 : 𝐵 –onto→ 𝐴 )
58 imassrn ⊢ ( ◡ 𝑓 “ 𝑧 ) ⊆ ran ◡ 𝑓
59 forn ⊢ ( ◡ 𝑓 : 𝐵 –onto→ 𝐴 → ran ◡ 𝑓 = 𝐴 )
60 58 59 sseqtrid ⊢ ( ◡ 𝑓 : 𝐵 –onto→ 𝐴 → ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 )
61 57 60 syl ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 )
62 56 61 jctild ⊢ ( ◡ 𝑓 : 𝐵 –1-1-onto→ 𝐴 → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶 ) → ( ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) ) )
63 46 62 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶 ) → ( ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) ) )
64 elin ⊢ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
65 51 elpw ⊢ ( 𝑧 ∈ 𝒫 𝐵 ↔ 𝑧 ⊆ 𝐵 )
66 breq1 ⊢ ( 𝑥 = 𝑧 → ( 𝑥 ≈ 𝐶 ↔ 𝑧 ≈ 𝐶 ) )
67 51 66 elab ⊢ ( 𝑧 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ↔ 𝑧 ≈ 𝐶 )
68 65 67 anbi12i ⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶 ) )
69 64 68 bitri ⊢ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( 𝑧 ⊆ 𝐵 ∧ 𝑧 ≈ 𝐶 ) )
70 elin ⊢ ( ( ◡ 𝑓 “ 𝑧 ) ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( ◡ 𝑓 “ 𝑧 ) ∈ 𝒫 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
71 3 cnvex ⊢ ◡ 𝑓 ∈ V
72 71 imaex ⊢ ( ◡ 𝑓 “ 𝑧 ) ∈ V
73 72 elpw ⊢ ( ( ◡ 𝑓 “ 𝑧 ) ∈ 𝒫 𝐴 ↔ ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 )
74 breq1 ⊢ ( 𝑥 = ( ◡ 𝑓 “ 𝑧 ) → ( 𝑥 ≈ 𝐶 ↔ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) )
75 72 74 elab ⊢ ( ( ◡ 𝑓 “ 𝑧 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ↔ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 )
76 73 75 anbi12i ⊢ ( ( ( ◡ 𝑓 “ 𝑧 ) ∈ 𝒫 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) )
77 70 76 bitri ⊢ ( ( ◡ 𝑓 “ 𝑧 ) ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ↔ ( ( ◡ 𝑓 “ 𝑧 ) ⊆ 𝐴 ∧ ( ◡ 𝑓 “ 𝑧 ) ≈ 𝐶 ) )
78 63 69 77 3imtr4g ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → ( ◡ 𝑓 “ 𝑧 ) ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) )
79 simpl ⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑧 ∈ 𝒫 𝐵 )
80 79 elpwid ⊢ ( ( 𝑧 ∈ 𝒫 𝐵 ∧ 𝑧 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑧 ⊆ 𝐵 )
81 64 80 sylbi ⊢ ( 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑧 ⊆ 𝐵 )
82 imaeq2 ⊢ ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) → ( 𝑓 “ 𝑦 ) = ( 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) )
83 f1orel ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → Rel 𝑓 )
84 dfrel2 ⊢ ( Rel 𝑓 ↔ ◡ ◡ 𝑓 = 𝑓 )
85 83 84 sylib ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ ◡ 𝑓 = 𝑓 )
86 85 imaeq1d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ◡ ◡ 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) = ( 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) )
87 86 adantr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) → ( ◡ ◡ 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) = ( 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) )
88 46 47 syl ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ◡ 𝑓 : 𝐵 –1-1→ 𝐴 )
89 f1imacnv ⊢ ( ( ◡ 𝑓 : 𝐵 –1-1→ 𝐴 ∧ 𝑧 ⊆ 𝐵 ) → ( ◡ ◡ 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) = 𝑧 )
90 88 89 sylan ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) → ( ◡ ◡ 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) = 𝑧 )
91 87 90 eqtr3d ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) → ( 𝑓 “ ( ◡ 𝑓 “ 𝑧 ) ) = 𝑧 )
92 82 91 sylan9eqr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ) → ( 𝑓 “ 𝑦 ) = 𝑧 )
93 92 eqcomd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) ∧ 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ) → 𝑧 = ( 𝑓 “ 𝑦 ) )
94 93 ex ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ⊆ 𝐵 ) → ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) → 𝑧 = ( 𝑓 “ 𝑦 ) ) )
95 81 94 sylan2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) → ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) → 𝑧 = ( 𝑓 “ 𝑦 ) ) )
96 95 adantrl ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∧ 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) ) → ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) → 𝑧 = ( 𝑓 “ 𝑦 ) ) )
97 simpl ⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑦 ∈ 𝒫 𝐴 )
98 97 elpwid ⊢ ( ( 𝑦 ∈ 𝒫 𝐴 ∧ 𝑦 ∈ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑦 ⊆ 𝐴 )
99 32 98 sylbi ⊢ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) → 𝑦 ⊆ 𝐴 )
100 imaeq2 ⊢ ( 𝑧 = ( 𝑓 “ 𝑦 ) → ( ◡ 𝑓 “ 𝑧 ) = ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) )
101 f1imacnv ⊢ ( ( 𝑓 : 𝐴 –1-1→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) = 𝑦 )
102 17 101 sylan ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → ( ◡ 𝑓 “ ( 𝑓 “ 𝑦 ) ) = 𝑦 )
103 100 102 sylan9eqr ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑧 = ( 𝑓 “ 𝑦 ) ) → ( ◡ 𝑓 “ 𝑧 ) = 𝑦 )
104 103 eqcomd ⊢ ( ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) ∧ 𝑧 = ( 𝑓 “ 𝑦 ) ) → 𝑦 = ( ◡ 𝑓 “ 𝑧 ) )
105 104 ex ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) → ( 𝑧 = ( 𝑓 “ 𝑦 ) → 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ) )
106 99 105 sylan2 ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) → ( 𝑧 = ( 𝑓 “ 𝑦 ) → 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ) )
107 106 adantrr ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∧ 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) ) → ( 𝑧 = ( 𝑓 “ 𝑦 ) → 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ) )
108 96 107 impbid ⊢ ( ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 ∧ ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∧ 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) ) → ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ↔ 𝑧 = ( 𝑓 “ 𝑦 ) ) )
109 108 ex ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( ( 𝑦 ∈ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ∧ 𝑧 ∈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ) → ( 𝑦 = ( ◡ 𝑓 “ 𝑧 ) ↔ 𝑧 = ( 𝑓 “ 𝑦 ) ) ) )
110 8 16 45 78 109 en3d ⊢ ( 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ≈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
111 110 exlimiv ⊢ ( ∃ 𝑓 𝑓 : 𝐴 –1-1-onto→ 𝐵 → ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ≈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
112 1 111 sylbi ⊢ ( 𝐴 ≈ 𝐵 → ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) ≈ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) )
113 df-pw ⊢ 𝒫 𝐴 = { 𝑥 ∣ 𝑥 ⊆ 𝐴 }
114 113 ineq1i ⊢ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = ( { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } )
115 inab ⊢ ( { 𝑥 ∣ 𝑥 ⊆ 𝐴 } ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶 ) }
116 114 115 eqtri ⊢ ( 𝒫 𝐴 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶 ) }
117 df-pw ⊢ 𝒫 𝐵 = { 𝑥 ∣ 𝑥 ⊆ 𝐵 }
118 117 ineq1i ⊢ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = ( { 𝑥 ∣ 𝑥 ⊆ 𝐵 } ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } )
119 inab ⊢ ( { 𝑥 ∣ 𝑥 ⊆ 𝐵 } ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = { 𝑥 ∣ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶 ) }
120 118 119 eqtri ⊢ ( 𝒫 𝐵 ∩ { 𝑥 ∣ 𝑥 ≈ 𝐶 } ) = { 𝑥 ∣ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶 ) }
121 112 116 120 3brtr3g ⊢ ( 𝐴 ≈ 𝐵 → { 𝑥 ∣ ( 𝑥 ⊆ 𝐴 ∧ 𝑥 ≈ 𝐶 ) } ≈ { 𝑥 ∣ ( 𝑥 ⊆ 𝐵 ∧ 𝑥 ≈ 𝐶 ) } )