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 ffvelrnd 
 |-  ( ( ( 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 weeq2 
 |-  ( x = C -> ( r We x <-> r We C ) )
64 weeq1 
 |-  ( r = ( ( W ` B ) i^i ( C X. C ) ) -> ( r We C <-> ( ( W ` B ) i^i ( C X. C ) ) We C ) )
65 63 64 sylan9bb 
 |-  ( ( x = C /\ r = ( ( W ` B ) i^i ( C X. C ) ) ) -> ( r We x <-> ( ( W ` B ) i^i ( C X. C ) ) We C ) )
66 59 62 65 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 ) ) )
67 56 57 66 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 ) )
68 44 46 52 67 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 ) } )
69 68 1 eleqtrrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. e. O )
70 8 43 ssexd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> B e. _V )
71 53 a1i 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) e. _V )
72 simpl 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> x = B )
73 72 sseq1d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( x C_ A <-> B C_ A ) )
74 simpr 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> r = ( W ` B ) )
75 72 sqxpeqd 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( x X. x ) = ( B X. B ) )
76 74 75 sseq12d 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( r C_ ( x X. x ) <-> ( W ` B ) C_ ( B X. B ) ) )
77 weeq2 
 |-  ( x = B -> ( r We x <-> r We B ) )
78 weeq1 
 |-  ( r = ( W ` B ) -> ( r We B <-> ( W ` B ) We B ) )
79 77 78 sylan9bb 
 |-  ( ( x = B /\ r = ( W ` B ) ) -> ( r We x <-> ( W ` B ) We B ) )
80 73 76 79 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 ) ) )
81 80 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 ) ) )
82 70 71 81 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 ) ) )
83 43 36 48 82 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 ) } )
84 83 1 eleqtrrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. B , ( W ` B ) >. e. O )
85 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 ) >. ) )
86 31 69 84 85 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 ) >. ) )
87 30 86 mpbid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. )
88 56 57 opth1 
 |-  ( <. C , ( ( W ` B ) i^i ( C X. C ) ) >. = <. B , ( W ` B ) >. -> C = B )
89 87 88 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> C = B )
90 20 89 eleqtrrd 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) e. C )
91 90 4 eleqtrdi 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) e. ( `' ( W ` B ) " { ( B F ( W ` B ) ) } ) )
92 ovex 
 |-  ( B F ( W ` B ) ) e. _V
93 92 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 ) ) ) )
94 20 93 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 ) ) ) )
95 91 94 mpbid 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
96 weso 
 |-  ( ( W ` B ) We B -> ( W ` B ) Or B )
97 48 96 syl 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> ( W ` B ) Or B )
98 sonr 
 |-  ( ( ( W ` B ) Or B /\ ( B F ( W ` B ) ) e. B ) -> -. ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
99 97 20 98 syl2anc 
 |-  ( ( A e. V /\ F : O -1-1-> A ) -> -. ( B F ( W ` B ) ) ( W ` B ) ( B F ( W ` B ) ) )
100 95 99 pm2.65da 
 |-  ( A e. V -> -. F : O -1-1-> A )