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 f f : A 1-1 onto B
2 f1odm f : A 1-1 onto B dom f = A
3 vex f V
4 3 dmex dom f V
5 2 4 syl6eqelr f : A 1-1 onto B 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 onto B 𝒫 A x | x C V
9 f1ofo f : A 1-1 onto B f : A onto B
10 forn f : A onto B ran f = B
11 9 10 syl f : A 1-1 onto B ran f = B
12 3 rnex ran f V
13 11 12 syl6eqelr f : A 1-1 onto B 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 onto B 𝒫 B x | x C V
17 f1of1 f : A 1-1 onto B f : A 1-1 B
18 17 adantr f : A 1-1 onto B y A f : A 1-1 B
19 13 adantr f : A 1-1 onto B y A B V
20 simpr f : A 1-1 onto B y A y A
21 vex y V
22 21 a1i f : A 1-1 onto B y A y V
23 f1imaen2g f : A 1-1 B B V y A y V f y y
24 18 19 20 22 23 syl22anc f : A 1-1 onto B y A f y y
25 entr f y y y C f y C
26 24 25 sylan f : A 1-1 onto B y A y C f y C
27 26 expl f : A 1-1 onto B y A y C f y C
28 imassrn f y ran f
29 28 10 sseqtrid f : A onto B f y B
30 9 29 syl f : A 1-1 onto B f y B
31 27 30 jctild f : A 1-1 onto B y A y C f y B f y 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 f y 𝒫 B x | x C f y 𝒫 B f y x | x C
39 3 imaex f y V
40 39 elpw f y 𝒫 B f y B
41 breq1 x = f y x C f y C
42 39 41 elab f y x | x C f y C
43 40 42 anbi12i f y 𝒫 B f y x | x C f y B f y C
44 38 43 bitri f y 𝒫 B x | x C f y B f y C
45 31 37 44 3imtr4g f : A 1-1 onto B y 𝒫 A x | x C f y 𝒫 B x | x C
46 f1ocnv f : A 1-1 onto B f -1 : B 1-1 onto A
47 f1of1 f -1 : B 1-1 onto A f -1 : B 1-1 A
48 f1f1orn f -1 : B 1-1 A f -1 : B 1-1 onto ran f -1
49 f1of1 f -1 : B 1-1 onto ran f -1 f -1 : B 1-1 ran f -1
50 47 48 49 3syl f -1 : B 1-1 onto A f -1 : B 1-1 ran f -1
51 vex z V
52 51 f1imaen f -1 : B 1-1 ran f -1 z B f -1 z z
53 50 52 sylan f -1 : B 1-1 onto A z B f -1 z z
54 entr f -1 z z z C f -1 z C
55 53 54 sylan f -1 : B 1-1 onto A z B z C f -1 z C
56 55 expl f -1 : B 1-1 onto A z B z C f -1 z C
57 f1ofo f -1 : B 1-1 onto A f -1 : B onto A
58 imassrn f -1 z ran f -1
59 forn f -1 : B onto A ran f -1 = A
60 58 59 sseqtrid f -1 : B onto A f -1 z A
61 57 60 syl f -1 : B 1-1 onto A f -1 z A
62 56 61 jctild f -1 : B 1-1 onto A z B z C f -1 z A f -1 z C
63 46 62 syl f : A 1-1 onto B z B z C f -1 z A f -1 z 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 -1 z 𝒫 A x | x C f -1 z 𝒫 A f -1 z x | x C
71 3 cnvex f -1 V
72 71 imaex f -1 z V
73 72 elpw f -1 z 𝒫 A f -1 z A
74 breq1 x = f -1 z x C f -1 z C
75 72 74 elab f -1 z x | x C f -1 z C
76 73 75 anbi12i f -1 z 𝒫 A f -1 z x | x C f -1 z A f -1 z C
77 70 76 bitri f -1 z 𝒫 A x | x C f -1 z A f -1 z C
78 63 69 77 3imtr4g f : A 1-1 onto B z 𝒫 B x | x C f -1 z 𝒫 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 -1 z f y = f f -1 z
83 f1orel f : A 1-1 onto B Rel f
84 dfrel2 Rel f f -1 -1 = f
85 83 84 sylib f : A 1-1 onto B f -1 -1 = f
86 85 imaeq1d f : A 1-1 onto B f -1 -1 f -1 z = f f -1 z
87 86 adantr f : A 1-1 onto B z B f -1 -1 f -1 z = f f -1 z
88 46 47 syl f : A 1-1 onto B f -1 : B 1-1 A
89 f1imacnv f -1 : B 1-1 A z B f -1 -1 f -1 z = z
90 88 89 sylan f : A 1-1 onto B z B f -1 -1 f -1 z = z
91 87 90 eqtr3d f : A 1-1 onto B z B f f -1 z = z
92 82 91 sylan9eqr f : A 1-1 onto B z B y = f -1 z f y = z
93 92 eqcomd f : A 1-1 onto B z B y = f -1 z z = f y
94 93 ex f : A 1-1 onto B z B y = f -1 z z = f y
95 81 94 sylan2 f : A 1-1 onto B z 𝒫 B x | x C y = f -1 z z = f y
96 95 adantrl f : A 1-1 onto B y 𝒫 A x | x C z 𝒫 B x | x C y = f -1 z z = f y
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 = f y f -1 z = f -1 f y
101 f1imacnv f : A 1-1 B y A f -1 f y = y
102 17 101 sylan f : A 1-1 onto B y A f -1 f y = y
103 100 102 sylan9eqr f : A 1-1 onto B y A z = f y f -1 z = y
104 103 eqcomd f : A 1-1 onto B y A z = f y y = f -1 z
105 104 ex f : A 1-1 onto B y A z = f y y = f -1 z
106 99 105 sylan2 f : A 1-1 onto B y 𝒫 A x | x C z = f y y = f -1 z
107 106 adantrr f : A 1-1 onto B y 𝒫 A x | x C z 𝒫 B x | x C z = f y y = f -1 z
108 96 107 impbid f : A 1-1 onto B y 𝒫 A x | x C z 𝒫 B x | x C y = f -1 z z = f y
109 108 ex f : A 1-1 onto B y 𝒫 A x | x C z 𝒫 B x | x C y = f -1 z z = f y
110 8 16 45 78 109 en3d f : A 1-1 onto B 𝒫 A x | x C 𝒫 B x | x C
111 110 exlimiv f f : A 1-1 onto B 𝒫 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