# 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 ( 𝐴𝐵 → { 𝑥 ∣ ( 𝑥𝐴𝑥𝐶 ) } ≈ { 𝑥 ∣ ( 𝑥𝐵𝑥𝐶 ) } )