Metamath Proof Explorer

Theorem canthnumlem

Description: Lemma for canthnum . (Contributed by Mario Carneiro, 19-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 canthnumlem 
|- ( A e. V -> -. F : ( ~P A i^i dom card ) -1-1-> A )

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 f1f 
 |-  ( F : ( ~P A i^i dom card ) -1-1-> A -> F : ( ~P A i^i dom card ) --> A )
5 ssid 
 |-  ( ~P A i^i dom card ) C_ ( ~P A i^i dom card )
6 1 2 3 canth4 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) --> A /\ ( ~P A i^i dom card ) C_ ( ~P A i^i dom card ) ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
7 5 6 mp3an3 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) --> A ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
8 4 7 sylan2 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B C_ A /\ C C. B /\ ( F ` B ) = ( F ` C ) ) )
9 8 simp3d 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( F ` B ) = ( F ` C ) )
10 simpr 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> F : ( ~P A i^i dom card ) -1-1-> A )
11 8 simp1d 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B C_ A )
12 elpw2g 
 |-  ( A e. V -> ( B e. ~P A <-> B C_ A ) )
13 12 adantr 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B e. ~P A <-> B C_ A ) )
14 11 13 mpbird 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. ~P A )
15 eqid 
 |-  B = B
16 eqid 
 |-  ( W ` B ) = ( W ` B )
17 15 16 pm3.2i 
 |-  ( B = B /\ ( W ` B ) = ( W ` B ) )
18 simpl 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> A e. V )
19 10 4 syl 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> F : ( ~P A i^i dom card ) --> A )
20 19 ffvelrnda 
 |-  ( ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) /\ x e. ( ~P A i^i dom card ) ) -> ( F ` x ) e. A )
21 1 18 20 2 fpwwe 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( B W ( W ` B ) /\ ( F ` B ) e. B ) <-> ( B = B /\ ( W ` B ) = ( W ` B ) ) ) )
22 17 21 mpbiri 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( B W ( W ` B ) /\ ( F ` B ) e. B ) )
23 22 simpld 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B W ( W ` B ) )
24 1 18 fpwwelem 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( 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 ) ) ) )
25 23 24 mpbid 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B ( F ` ( `' ( W ` B ) " { y } ) ) = y ) ) )
26 25 simprld 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( W ` B ) We B )
27 fvex 
 |-  ( W ` B ) e. _V
28 weeq1 
 |-  ( r = ( W ` B ) -> ( r We B <-> ( W ` B ) We B ) )
29 27 28 spcev 
 |-  ( ( W ` B ) We B -> E. r r We B )
30 26 29 syl 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> E. r r We B )
31 ween 
 |-  ( B e. dom card <-> E. r r We B )
32 30 31 sylibr 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. dom card )
33 14 32 elind 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B e. ( ~P A i^i dom card ) )
34 8 simp2d 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C. B )
35 34 pssssd 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C_ B )
36 35 11 sstrd 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C C_ A )
37 elpw2g 
 |-  ( A e. V -> ( C e. ~P A <-> C C_ A ) )
38 37 adantr 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( C e. ~P A <-> C C_ A ) )
39 36 38 mpbird 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. ~P A )
40 ssnum 
 |-  ( ( B e. dom card /\ C C_ B ) -> C e. dom card )
41 32 35 40 syl2anc 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. dom card )
42 39 41 elind 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C e. ( ~P A i^i dom card ) )
43 f1fveq 
 |-  ( ( F : ( ~P A i^i dom card ) -1-1-> A /\ ( B e. ( ~P A i^i dom card ) /\ C e. ( ~P A i^i dom card ) ) ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
44 10 33 42 43 syl12anc 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> ( ( F ` B ) = ( F ` C ) <-> B = C ) )
45 9 44 mpbid 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B = C )
46 34 pssned 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> C =/= B )
47 46 necomd 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> B =/= C )
48 47 neneqd 
 |-  ( ( A e. V /\ F : ( ~P A i^i dom card ) -1-1-> A ) -> -. B = C )
49 45 48 pm2.65da 
 |-  ( A e. V -> -. F : ( ~P A i^i dom card ) -1-1-> A )