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 C_ A /\ x ~~ C ) } ~~ { x | ( x C_ B /\ x ~~ C ) } )

Proof

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