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