# 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 )`
` |-  ( ( f : A -1-1-onto-> B /\ y C_ A ) -> f : A -1-1-> B )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) ) )`
` |-  ( ( 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 ) } )`