Metamath Proof Explorer

Theorem fpwwe2

Description: Given any function F from well-orderings of subsets of A to A , there is a unique well-ordered subset <. X , ( WX ) >. which "agrees" with F in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a . Theorem 1.1 of KanamoriPincus p. 415. (Contributed by Mario Carneiro, 18-May-2015) (Revised by AV, 20-Jul-2024)

Ref Expression
Hypotheses fpwwe2.1 
|- 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 ) ) }
fpwwe2.2 
|- ( ph -> A e. V )
fpwwe2.3 
|- ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
fpwwe2.4 
|- X = U. dom W
Assertion fpwwe2 
|- ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )

Proof

Step Hyp Ref Expression
1 fpwwe2.1 
 |-  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 ) ) }
2 fpwwe2.2 
 |-  ( ph -> A e. V )
3 fpwwe2.3 
 |-  ( ( ph /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
4 fpwwe2.4 
 |-  X = U. dom W
5 1 2 3 4 fpwwe2lem10 
 |-  ( ph -> W : dom W --> ~P ( X X. X ) )
6 5 ffund 
 |-  ( ph -> Fun W )
7 funbrfv2b 
 |-  ( Fun W -> ( Y W R <-> ( Y e. dom W /\ ( W ` Y ) = R ) ) )
8 6 7 syl 
 |-  ( ph -> ( Y W R <-> ( Y e. dom W /\ ( W ` Y ) = R ) ) )
9 8 simprbda 
 |-  ( ( ph /\ Y W R ) -> Y e. dom W )
10 9 adantrr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y e. dom W )
11 elssuni 
 |-  ( Y e. dom W -> Y C_ U. dom W )
12 11 4 sseqtrrdi 
 |-  ( Y e. dom W -> Y C_ X )
13 10 12 syl 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y C_ X )
14 simpl 
 |-  ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) -> X C_ Y )
15 14 a1i 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) -> X C_ Y ) )
16 simplrr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( Y F R ) e. Y )
17 2 adantr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> A e. V )
18 17 adantr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> A e. V )
19 1 2 3 4 fpwwe2lem11 
 |-  ( ph -> X e. dom W )
20 funfvbrb 
 |-  ( Fun W -> ( X e. dom W <-> X W ( W ` X ) ) )
21 6 20 syl 
 |-  ( ph -> ( X e. dom W <-> X W ( W ` X ) ) )
22 19 21 mpbid 
 |-  ( ph -> X W ( W ` X ) )
23 1 2 fpwwe2lem2 
 |-  ( ph -> ( X W ( W ` X ) <-> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) ) )
24 22 23 mpbid 
 |-  ( ph -> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) )
25 24 ad2antrr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) /\ ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) ) )
26 25 simpld 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) )
27 26 simpld 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X C_ A )
28 18 27 ssexd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X e. _V )
29 28 difexd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) e. _V )
30 25 simprd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) )
31 30 simpld 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) We X )
32 wefr 
 |-  ( ( W ` X ) We X -> ( W ` X ) Fr X )
33 31 32 syl 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) Fr X )
34 difssd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) C_ X )
35 fri 
 |-  ( ( ( ( X \ Y ) e. _V /\ ( W ` X ) Fr X ) /\ ( ( X \ Y ) C_ X /\ ( X \ Y ) =/= (/) ) ) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z )
36 35 expr 
 |-  ( ( ( ( X \ Y ) e. _V /\ ( W ` X ) Fr X ) /\ ( X \ Y ) C_ X ) -> ( ( X \ Y ) =/= (/) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z ) )
37 29 33 34 36 syl21anc 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X \ Y ) =/= (/) -> E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z ) )
38 ssdif0 
 |-  ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) )
39 indif1 
 |-  ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y )
40 39 eqeq1i 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) )
41 disj 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) )
42 vex 
 |-  w e. _V
43 42 eliniseg 
 |-  ( z e. _V -> ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z ) )
44 43 elv 
 |-  ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z )
45 44 notbii 
 |-  ( -. w e. ( `' ( W ` X ) " { z } ) <-> -. w ( W ` X ) z )
46 45 ralbii 
 |-  ( A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
47 41 46 bitri 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
48 38 40 47 3bitr2i 
 |-  ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
49 cnvimass 
 |-  ( `' ( W ` X ) " { z } ) C_ dom ( W ` X )
50 26 simprd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( W ` X ) C_ ( X X. X ) )
51 dmss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
52 50 51 syl 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> dom ( W ` X ) C_ dom ( X X. X ) )
53 dmxpid 
 |-  dom ( X X. X ) = X
54 52 53 sseqtrdi 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> dom ( W ` X ) C_ X )
55 49 54 sstrid 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( `' ( W ` X ) " { z } ) C_ X )
56 sseqin2 
 |-  ( ( `' ( W ` X ) " { z } ) C_ X <-> ( X i^i ( `' ( W ` X ) " { z } ) ) = ( `' ( W ` X ) " { z } ) )
57 55 56 sylib 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X i^i ( `' ( W ` X ) " { z } ) ) = ( `' ( W ` X ) " { z } ) )
58 57 sseq1d 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> ( `' ( W ` X ) " { z } ) C_ Y ) )
59 48 58 bitr3id 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( A. w e. ( X \ Y ) -. w ( W ` X ) z <-> ( `' ( W ` X ) " { z } ) C_ Y ) )
60 59 rexbidv 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z <-> E. z e. ( X \ Y ) ( `' ( W ` X ) " { z } ) C_ Y ) )
61 eldifn 
 |-  ( z e. ( X \ Y ) -> -. z e. Y )
62 61 ad2antrl 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> -. z e. Y )
63 eleq1w 
 |-  ( w = z -> ( w e. Y <-> z e. Y ) )
64 63 notbid 
 |-  ( w = z -> ( -. w e. Y <-> -. z e. Y ) )
65 62 64 syl5ibrcom 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w = z -> -. w e. Y ) )
66 65 con2d 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w e. Y -> -. w = z ) )
67 66 imp 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. w = z )
68 62 adantr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. z e. Y )
69 simprr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) )
70 69 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) )
71 70 breqd 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w <-> z ( ( W ` X ) i^i ( X X. Y ) ) w ) )
72 eldifi 
 |-  ( z e. ( X \ Y ) -> z e. X )
73 72 ad2antrl 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> z e. X )
74 73 adantr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> z e. X )
75 simpr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. Y )
76 brxp 
 |-  ( z ( X X. Y ) w <-> ( z e. X /\ w e. Y ) )
77 74 75 76 sylanbrc 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> z ( X X. Y ) w )
78 brin 
 |-  ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> ( z ( W ` X ) w /\ z ( X X. Y ) w ) )
79 78 rbaib 
 |-  ( z ( X X. Y ) w -> ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> z ( W ` X ) w ) )
80 77 79 syl 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> z ( W ` X ) w ) )
81 71 80 bitrd 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w <-> z ( W ` X ) w ) )
82 1 2 fpwwe2lem2 
 |-  ( ph -> ( Y W R <-> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) ) )
83 82 biimpa 
 |-  ( ( ph /\ Y W R ) -> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) )
84 83 adantrr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( Y C_ A /\ R C_ ( Y X. Y ) ) /\ ( R We Y /\ A. y e. Y [. ( `' R " { y } ) / u ]. ( u F ( R i^i ( u X. u ) ) ) = y ) ) )
85 84 simpld 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y C_ A /\ R C_ ( Y X. Y ) ) )
86 85 simprd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R C_ ( Y X. Y ) )
87 86 ad3antrrr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> R C_ ( Y X. Y ) )
88 87 ssbrd 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w -> z ( Y X. Y ) w ) )
89 brxp 
 |-  ( z ( Y X. Y ) w <-> ( z e. Y /\ w e. Y ) )
90 89 simplbi 
 |-  ( z ( Y X. Y ) w -> z e. Y )
91 88 90 syl6 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z R w -> z e. Y ) )
92 81 91 sylbird 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( z ( W ` X ) w -> z e. Y ) )
93 68 92 mtod 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> -. z ( W ` X ) w )
94 31 ad2antrr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( W ` X ) We X )
95 weso 
 |-  ( ( W ` X ) We X -> ( W ` X ) Or X )
96 94 95 syl 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( W ` X ) Or X )
97 13 ad2antrr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y C_ X )
98 97 sselda 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. X )
99 sotric 
 |-  ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> -. ( w = z \/ z ( W ` X ) w ) ) )
100 ioran 
 |-  ( -. ( w = z \/ z ( W ` X ) w ) <-> ( -. w = z /\ -. z ( W ` X ) w ) )
101 99 100 bitrdi 
 |-  ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> ( -. w = z /\ -. z ( W ` X ) w ) ) )
102 96 98 74 101 syl12anc 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> ( w ( W ` X ) z <-> ( -. w = z /\ -. z ( W ` X ) w ) ) )
103 67 93 102 mpbir2and 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w ( W ` X ) z )
104 103 44 sylibr 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ w e. Y ) -> w e. ( `' ( W ` X ) " { z } ) )
105 104 ex 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( w e. Y -> w e. ( `' ( W ` X ) " { z } ) ) )
106 105 ssrdv 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y C_ ( `' ( W ` X ) " { z } ) )
107 simprr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( `' ( W ` X ) " { z } ) C_ Y )
108 106 107 eqssd 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> Y = ( `' ( W ` X ) " { z } ) )
109 in32 
 |-  ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) = ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) )
110 simplrr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( X X. Y ) ) )
111 110 ineq1d 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( R i^i ( Y X. Y ) ) = ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) )
112 86 ad2antrr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R C_ ( Y X. Y ) )
113 dfss2 
 |-  ( R C_ ( Y X. Y ) <-> ( R i^i ( Y X. Y ) ) = R )
114 112 113 sylib 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( R i^i ( Y X. Y ) ) = R )
115 111 114 eqtr3d 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( ( W ` X ) i^i ( X X. Y ) ) i^i ( Y X. Y ) ) = R )
116 inss2 
 |-  ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( Y X. Y )
117 xpss1 
 |-  ( Y C_ X -> ( Y X. Y ) C_ ( X X. Y ) )
118 97 117 syl 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y X. Y ) C_ ( X X. Y ) )
119 116 118 sstrid 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( X X. Y ) )
120 dfss2 
 |-  ( ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( X X. Y ) <-> ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) ) = ( ( W ` X ) i^i ( Y X. Y ) ) )
121 119 120 sylib 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( ( W ` X ) i^i ( Y X. Y ) ) i^i ( X X. Y ) ) = ( ( W ` X ) i^i ( Y X. Y ) ) )
122 109 115 121 3eqtr3a 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( Y X. Y ) ) )
123 108 sqxpeqd 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y X. Y ) = ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) )
124 123 ineq2d 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( W ` X ) i^i ( Y X. Y ) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) )
125 122 124 eqtrd 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> R = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) )
126 108 125 oveq12d 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y F R ) = ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) )
127 18 adantr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> A e. V )
128 22 adantr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W ( W ` X ) )
129 128 ad2antrr 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> X W ( W ` X ) )
130 1 127 129 fpwwe2lem3 
 |-  ( ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) /\ z e. X ) -> ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) = z )
131 73 130 mpdan 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( ( `' ( W ` X ) " { z } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { z } ) X. ( `' ( W ` X ) " { z } ) ) ) ) = z )
132 126 131 eqtrd 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> ( Y F R ) = z )
133 132 62 eqneltrd 
 |-  ( ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) /\ ( z e. ( X \ Y ) /\ ( `' ( W ` X ) " { z } ) C_ Y ) ) -> -. ( Y F R ) e. Y )
134 133 rexlimdvaa 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) ( `' ( W ` X ) " { z } ) C_ Y -> -. ( Y F R ) e. Y ) )
135 60 134 sylbid 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( E. z e. ( X \ Y ) A. w e. ( X \ Y ) -. w ( W ` X ) z -> -. ( Y F R ) e. Y ) )
136 37 135 syld 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( X \ Y ) =/= (/) -> -. ( Y F R ) e. Y ) )
137 136 necon4ad 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( ( Y F R ) e. Y -> ( X \ Y ) = (/) ) )
138 16 137 mpd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) = (/) )
139 ssdif0 
 |-  ( X C_ Y <-> ( X \ Y ) = (/) )
140 138 139 sylibr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X C_ Y )
141 140 ex 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) -> X C_ Y ) )
142 3 adantlr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
143 simprl 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y W R )
144 1 17 142 128 143 fpwwe2lem9 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( X C_ Y /\ ( W ` X ) = ( R i^i ( Y X. X ) ) ) \/ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) )
145 15 141 144 mpjaod 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X C_ Y )
146 13 145 eqssd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y = X )
147 6 adantr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Fun W )
148 146 143 eqbrtrrd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W R )
149 funbrfv 
 |-  ( Fun W -> ( X W R -> ( W ` X ) = R ) )
150 147 148 149 sylc 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( W ` X ) = R )
151 150 eqcomd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R = ( W ` X ) )
152 146 151 jca 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y = X /\ R = ( W ` X ) ) )
153 152 ex 
 |-  ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) -> ( Y = X /\ R = ( W ` X ) ) ) )
154 1 2 3 4 fpwwe2lem12 
 |-  ( ph -> ( X F ( W ` X ) ) e. X )
155 22 154 jca 
 |-  ( ph -> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) )
156 breq12 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R <-> X W ( W ` X ) ) )
157 oveq12 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( Y F R ) = ( X F ( W ` X ) ) )
158 simpl 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> Y = X )
159 157 158 eleq12d 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y F R ) e. Y <-> ( X F ( W ` X ) ) e. X ) )
160 156 159 anbi12d 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) ) )
161 155 160 syl5ibrcom 
 |-  ( ph -> ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R /\ ( Y F R ) e. Y ) ) )
162 153 161 impbid 
 |-  ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )