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 ⊢A≈B→x|x⊆A∧x≈C≈x|x⊆B∧x≈C

Proof

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