Metamath Proof Explorer

Theorem canthwelem

Description: Lemma for canthwe . (Contributed by Mario Carneiro, 31-May-2015)

Ref Expression
Hypotheses canthwe.1 
|- O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
canthwe.2 
|- W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
canthwe.3 
|- B = U. dom W
canthwe.4 
|- C = ( `' ( W ` B ) " { ( B F ( W ` B ) ) } )
Assertion canthwelem 
|- ( A e. V -> -. F : O -1-1-> A )

Proof

Step Hyp Ref Expression
1 canthwe.1 
 |-  O = { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) }
2 canthwe.2 
 |-  W = { <. x , r >. | ( ( x C_ A /\ r C_ ( x X. x ) ) /\ ( r We x /\ A. y e. x [. ( `' r " { y } ) / u ]. ( u F ( r i^i ( u X. u ) ) ) = y ) ) }
3 canthwe.3 
 |-  B = U. dom W
4 canthwe.4 
 |-  C = ( `' ( W ` B ) " { ( B F ( W ` B ) ) } )
5 eqid 
 |-  B = B
6 eqid 
 |-  ( W ` B ) = ( W ` B )
7 5 6 pm3.2i 
 |-  ( B = B /\ ( W ` B ) = ( W ` B ) )
8 simpl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> A e. V )
9 df-ov 
 |-  ( x F r ) = ( F ` <. x , r >. )
10 f1f 
 |-  ( F : O -1-1-> A -> F : O --> A )
11 10 ad2antlr 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> F : O --> A )
12 simpr 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) )
13 opabidw 
 |-  ( <. x , r >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) )
14 12 13 sylibr 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> <. x , r >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
15 14 1 eleqtrrdi 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> <. x , r >. e. O )
16 11 15 ffvelcdmd 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( F ` <. x , r >. ) e. A )
17 9 16 eqeltrid 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
18 2 8 17 3 fpwwe2 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( B W ( W ` B ) /\ ( B F ( W ` B ) ) e. B ) <-> ( B = B /\ ( W ` B ) = ( W ` B ) ) ) )
19 7 18 mpbiri 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B W ( W ` B ) /\ ( B F ( W ` B ) ) e. B ) )
20 19 simprd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) e. B )
21 4 4 xpeq12i 
 |-  ( C X. C ) = ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) X. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) )
22 21 ineq2i 
 |-  ( ( W ` B ) i^i ( C X. C ) ) = ( ( W ` B ) i^i ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) X. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) ) )
23 4 22 oveq12i 
 |-  ( C F ( ( W ` B ) i^i ( C X. C ) ) ) = ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) F ( ( W ` B ) i^i ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) X. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) ) ) )
24 19 simpld 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> B W ( W ` B ) )
25 2 8 24 fpwwe2lem3 
 |-  ( ( ( A e. V /\ F : O -1-1-> A ) /\ ( B F ( W ` B ) ) e. B ) -> ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) F ( ( W ` B ) i^i ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) X. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) ) ) ) = ( B F ( W ` B ) ) )
26 20 25 mpdan 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) F ( ( W ` B ) i^i ( ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) X. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) ) ) ) = ( B F ( W ` B ) ) )
27 23 26 eqtrid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( C F ( ( W ` B ) i^i ( C X. C ) ) ) = ( B F ( W ` B ) ) )
28 df-ov 
 |-  ( C F ( ( W ` B ) i^i ( C X. C ) ) ) = ( F ` <. C , ( ( W ` B ) i^i ( C X. C ) ) >. )
29 df-ov 
 |-  ( B F ( W ` B ) ) = ( F ` <. B , ( W ` B ) >. )
30 27 28 29 3eqtr3g 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( F ` <. C , ( ( W ` B ) i^i ( C X. C ) ) >. ) = ( F ` <. B , ( W ` B ) >. ) )
31 simpr 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> F : O -1-1-> A )
32 cnvimass 
 |-  ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) C_ dom ( W ` B )
33 2 8 fpwwe2lem2 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B W ( W ` B ) <-> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B [. ( `' ( W ` B ) " { y } ) / u ]. ( u F ( ( W ` B ) i^i ( u X. u ) ) ) = y ) ) ) )
34 24 33 mpbid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) /\ ( ( W ` B ) We B /\ A. y e. B [. ( `' ( W ` B ) " { y } ) / u ]. ( u F ( ( W ` B ) i^i ( u X. u ) ) ) = y ) ) )
35 34 simpld 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B C_ A /\ ( W ` B ) C_ ( B X. B ) ) )
36 35 simprd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) C_ ( B X. B ) )
37 dmss 
 |-  ( ( W ` B ) C_ ( B X. B ) -> dom ( W ` B ) C_ dom ( B X. B ) )
38 36 37 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> dom ( W ` B ) C_ dom ( B X. B ) )
39 dmxpss 
 |-  dom ( B X. B ) C_ B
40 38 39 sstrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> dom ( W ` B ) C_ B )
41 32 40 sstrid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) C_ B )
42 4 41 eqsstrid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> C C_ B )
43 35 simpld 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> B C_ A )
44 42 43 sstrd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> C C_ A )
45 inss2 
 |-  ( ( W ` B ) i^i ( C X. C ) ) C_ ( C X. C )
46 45 a1i 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( W ` B ) i^i ( C X. C ) ) C_ ( C X. C ) )
47 34 simprd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( W ` B ) We B /\ A. y e. B [. ( `' ( W ` B ) " { y } ) / u ]. ( u F ( ( W ` B ) i^i ( u X. u ) ) ) = y ) )
48 47 simpld 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) We B )
49 wess 
 |-  ( C C_ B -> ( ( W ` B ) We B -> ( W ` B ) We C ) )
50 42 48 49 sylc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) We C )
51 weinxp 
 |-  ( ( W ` B ) We C <-> ( ( W ` B ) i^i ( C X. C ) ) We C )
52 50 51 sylib 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( W ` B ) i^i ( C X. C ) ) We C )
53 fvex 
 |-  ( W ` B ) e. _V
54 53 cnvex 
 |-  `' ( W ` B ) e. _V
55 54 imaex 
 |-  ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) e. _V
56 4 55 eqeltri 
 |-  C e. _V
57 53 inex1 
 |-  ( ( W ` B ) i^i ( C X. C ) ) e. _V
58 simpl 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> x = C )
59 58 sseq1d 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( x C_ A <-> C C_ A ) )
60 simpr 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> r = ( ( W ` B ) i^i ( C X. C ) ) )
61 58 sqxpeqd 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( x X. x ) = ( C X. C ) )
62 60 61 sseq12d 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( r C_ ( x X. x ) <-> ( ( W ` B ) i^i ( C X. C ) ) C_ ( C X. C ) ) )
63 60 58 weeq12d 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( r We x <-> ( ( W ` B ) i^i ( C X. C ) ) We C ) )
64 59 62 63 3anbi123d 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( C C_ A /\ ( ( W ` B ) i^i ( C X. C ) ) C_ ( C X. C ) /\ ( ( W ` B ) i^i ( C X. C ) ) We C ) ) )
65 56 57 64 opelopaba 
 |-  ( <. C , ( ( W ` B ) i^i ( C X. C ) ) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( C C_ A /\ ( ( W ` B ) i^i ( C X. C ) ) C_ ( C X. C ) /\ ( ( W ` B ) i^i ( C X. C ) ) We C ) )
66 44 46 52 65 syl3anbrc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
67 66 1 eleqtrrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. e. O )
68 8 43 ssexd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> B e. _V )
69 53 a1i 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) e. _V )
70 simpl 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> x = B )
71 70 sseq1d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( x C_ A <-> B C_ A ) )
72 simpr 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> r = ( W ` B ) )
73 70 sqxpeqd 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( x X. x ) = ( B X. B ) )
74 72 73 sseq12d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( r C_ ( x X. x ) <-> ( W ` B ) C_ ( B X. B ) ) )
75 72 70 weeq12d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( r We x <-> ( W ` B ) We B ) )
76 71 74 75 3anbi123d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) <-> ( B C_ A /\ ( W ` B ) C_ ( B X. B ) /\ ( W ` B ) We B ) ) )
77 76 opelopabga 
 |-  ( ( B e. _V /\ ( W ` B ) e. _V ) -> ( <. B , ( W ` B ) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( B C_ A /\ ( W ` B ) C_ ( B X. B ) /\ ( W ` B ) We B ) ) )
78 68 69 77 syl2anc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( <. B , ( W ` B ) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } <-> ( B C_ A /\ ( W ` B ) C_ ( B X. B ) /\ ( W ` B ) We B ) ) )
79 43 36 48 78 mpbir3and 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. B , ( W ` B ) >. e. { <. x , r >. | ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) } )
80 79 1 eleqtrrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. B , ( W ` B ) >. e. O )
81 f1fveq 
 |-  ( ( F : O -1-1-> A /\ ( <. C , ( ( W ` B ) i^i ( C X. C ) ) >. e. O /\ <. B , ( W ` B ) >. e. O ) ) -> ( ( F ` <. C , ( ( W ` B ) i^i ( C X. C ) ) >. ) = ( F ` <. B , ( W ` B ) >. ) <-> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. ) )
82 31 67 80 81 syl12anc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( F ` <. C , ( ( W ` B ) i^i ( C X. C ) ) >. ) = ( F ` <. B , ( W ` B ) >. ) <-> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. ) )
83 30 82 mpbid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. )
84 56 57 opth1 
 |-  ( <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. -> C = B )
85 83 84 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> C = B )
86 20 85 eleqtrrd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) e. C )
87 86 4 eleqtrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) e. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) )
88 ovex 
 |-  ( B F ( W ` B ) ) e. _V
89 88 eliniseg 
 |-  ( ( B F ( W ` B ) ) e. B -> ( ( B F ( W ` B ) ) e. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) <-> ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) ) )
90 20 89 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( ( B F ( W ` B ) ) e. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) <-> ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) ) )
91 87 90 mpbid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
92 weso 
 |-  ( ( W ` B ) We B -> ( W ` B ) Or B )
93 48 92 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) Or B )
94 sonr 
 |-  ( ( ( W ` B ) Or B /\ ( B F ( W ` B ) ) e. B ) -> -. ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
95 93 20 94 syl2anc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> -. ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
96 91 95 pm2.65da 
 |-  ( A e. V -> -. F : O -1-1-> A )