Metamath Proof Explorer

Theorem canth4

Description: An "effective" form of Cantor's theorem canth . For any function F from the powerset of A to A , there are two definable sets B and C which witness non-injectivity of F . Corollary 1.3 of KanamoriPincus p. 416. (Contributed by Mario Carneiro, 18-May-2015)

Ref Expression
Hypotheses canth4.1 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
canth4.2 
|- B = U. dom W
canth4.3 
|- C = ( `' ( W ` B ) " { ( F ` B ) } )
Assertion canth4 
|- ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )

Proof

Step Hyp Ref Expression
1 canth4.1 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x ( F ` ( `' r " { y } ) ) = y ) ) }
2 canth4.2 
 |-  B = U. dom W
3 canth4.3 
 |-  C = ( `' ( W ` B ) " { ( F ` B ) } )
4 eqid 
 |-  B = B
5 eqid 
 |-  ( W ` B ) = ( W ` B )
6 4 5 pm3.2i 
 |-  ( B = B /\ ( W ` B ) = ( W ` B ) )
7 simp1 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> A e. V )
8 simpl2 
 |-  ( ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) /\ x e. ( ~P A i^i dom card ) ) -> F : D --> A )
9 simp3 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( ~P A i^i dom card ) C_ D )
10 9 sselda 
 |-  ( ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) /\ x e. ( ~P A i^i dom card ) ) -> x e. D )
11 8 10 ffvelrnd 
 |-  ( ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
12 1 7 11 2 fpwwe 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( ( B W ( W ` B ) /\ ( F ` B ) e. B ) <-> ( B = B /\ ( W ` B ) = ( W ` B ) ) ) )
13 6 12 mpbiri 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B W ( W ` B ) /\ ( F ` B ) e. B ) )
14 13 simpld 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> B W ( W ` B ) )
15 1 7 fpwwelem 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B W ( W ` B ) <-> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) ) ) )
16 14 15 mpbid 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) ) )
17 16 simpld 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) )
18 17 simpld 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> B C_ A )
19 cnvimass 
 |-  ( `' ( W ` B ) " { ( F ` B ) } ) C_ dom ( W ` B )
20 3 19 eqsstri 
 |-  C C_ dom ( W ` B )
21 17 simprd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( W ` B ) C_ ( B X. B ) )
22 dmss 
 |-  ( ( W ` B ) C_ ( B X. B ) -> dom ( W ` B ) C_ dom ( B X. B ) )
23 21 22 syl 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> dom ( W ` B ) C_ dom ( B X. B ) )
24 dmxpid 
 |-  dom ( B X. B ) = B
25 23 24 sseqtrdi 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> dom ( W ` B ) C_ B )
26 20 25 sstrid 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> C C_ B )
27 13 simprd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( F ` B ) e. B )
28 16 simprd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) )
29 28 simpld 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( W ` B ) We B )
30 weso 
 |-  ( ( W ` B ) We B -> ( W ` B ) Or B )
31 29 30 syl 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( W ` B ) Or B )
32 sonr 
 |-  ( ( ( W ` B ) Or B /\ ( F ` B ) e. B ) -> -. ( F ` B ) ( W ` B ) ( F ` B ) )
33 31 27 32 syl2anc 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> -. ( F ` B ) ( W ` B ) ( F ` B ) )
34 3 eleq2i 
 |-  ( ( F ` B ) e. C <-> ( F ` B ) e. ( `' ( W ` B ) " { ( F ` B ) } ) )
35 fvex 
 |-  ( F ` B ) e. _V
36 35 eliniseg 
 |-  ( ( F ` B ) e. _V -> ( ( F ` B ) e. ( `' ( W ` B ) " { ( F ` B ) } ) <-> ( F ` B ) ( W ` B ) ( F ` B ) ) )
37 35 36 ax-mp 
 |-  ( ( F ` B ) e. ( `' ( W ` B ) " { ( F ` B ) } ) <-> ( F ` B ) ( W ` B ) ( F ` B ) )
38 34 37 bitri 
 |-  ( ( F ` B ) e. C <-> ( F ` B ) ( W ` B ) ( F ` B ) )
39 33 38 sylnibr 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> -. ( F ` B ) e. C )
40 26 27 39 ssnelpssd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> C C. B )
41 sneq 
 |-  ( y = ( F ` B ) -> { y } = { ( F ` B ) } )
42 41 imaeq2d 
 |-  ( y = ( F ` B ) -> ( `' ( W ` B ) " { y } ) = ( `' ( W ` B ) " { ( F ` B ) } ) )
43 42 3 eqtr4di 
 |-  ( y = ( F ` B ) -> ( `' ( W ` B ) " { y } ) = C )
44 43 fveq2d 
 |-  ( y = ( F ` B ) -> ( F ` ( `' ( W ` B ) " { y } ) ) = ( F ` C ) )
45 id 
 |-  ( y = ( F ` B ) -> y = ( F ` B ) )
46 44 45 eqeq12d 
 |-  ( y = ( F ` B ) -> ( ( F ` ( `' ( W ` B ) " { y } ) ) = y <-> ( F ` C ) = ( F ` B ) ) )
47 28 simprd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y )
48 46 47 27 rspcdva 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( F ` C ) = ( F ` B ) )
49 48 eqcomd 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( F ` B ) = ( F ` C ) )
50 18 40 49 3jca 
 |-  ( ( A e. V /\ F : D --> A /\ ( ~P A i^i dom card ) C_ D ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )