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 difexg 
 |-  ( X e. _V -> ( X \ Y ) e. _V )
30 28 29 syl 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) e. _V )
31 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 ) )
32 31 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 )
33 wefr 
 |-  ( ( W ` X ) We X -> ( W ` X ) Fr X )
34 32 33 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 )
35 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 )
36 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 )
37 36 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 ) )
38 30 34 35 37 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 ) )
39 ssdif0 
 |-  ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) )
40 indif1 
 |-  ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y )
41 40 eqeq1i 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> ( ( X i^i ( `' ( W ` X ) " { z } ) ) \ Y ) = (/) )
42 disj 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) )
43 vex 
 |-  w e. _V
44 43 eliniseg 
 |-  ( z e. _V -> ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z ) )
45 44 elv 
 |-  ( w e. ( `' ( W ` X ) " { z } ) <-> w ( W ` X ) z )
46 45 notbii 
 |-  ( -. w e. ( `' ( W ` X ) " { z } ) <-> -. w ( W ` X ) z )
47 46 ralbii 
 |-  ( A. w e. ( X \ Y ) -. w e. ( `' ( W ` X ) " { z } ) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
48 42 47 bitri 
 |-  ( ( ( X \ Y ) i^i ( `' ( W ` X ) " { z } ) ) = (/) <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
49 39 41 48 3bitr2i 
 |-  ( ( X i^i ( `' ( W ` X ) " { z } ) ) C_ Y <-> A. w e. ( X \ Y ) -. w ( W ` X ) z )
50 cnvimass 
 |-  ( `' ( W ` X ) " { z } ) C_ dom ( W ` X )
51 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 ) )
52 dmss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
53 51 52 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 ) )
54 dmxpid 
 |-  dom ( X X. X ) = X
55 53 54 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 )
56 50 55 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 )
57 sseqin2 
 |-  ( ( `' ( W ` X ) " { z } ) C_ X <-> ( X i^i ( `' ( W ` X ) " { z } ) ) = ( `' ( W ` X ) " { z } ) )
58 56 57 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 } ) )
59 58 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 ) )
60 49 59 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 ) )
61 60 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 ) )
62 eldifn 
 |-  ( z e. ( X \ Y ) -> -. z e. Y )
63 62 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 )
64 eleq1w 
 |-  ( w = z -> ( w e. Y <-> z e. Y ) )
65 64 notbid 
 |-  ( w = z -> ( -. w e. Y <-> -. z e. Y ) )
66 63 65 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 ) )
67 66 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 ) )
68 67 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 )
69 63 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 )
70 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 ) ) )
71 70 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 ) ) )
72 71 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 ) )
73 eldifi 
 |-  ( z e. ( X \ Y ) -> z e. X )
74 73 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 )
75 74 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 )
76 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 )
77 brxp 
 |-  ( z ( X X. Y ) w <-> ( z e. X /\ w e. Y ) )
78 75 76 77 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 )
79 brin 
 |-  ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> ( z ( W ` X ) w /\ z ( X X. Y ) w ) )
80 79 rbaib 
 |-  ( z ( X X. Y ) w -> ( z ( ( W ` X ) i^i ( X X. Y ) ) w <-> z ( W ` X ) w ) )
81 78 80 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 ) )
82 72 81 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 ) )
83 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 ) ) ) )
84 83 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 ) ) )
85 84 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 ) ) )
86 85 simpld 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y C_ A /\ R C_ ( Y X. Y ) ) )
87 86 simprd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R C_ ( Y X. Y ) )
88 87 ad5ant12 
 |-  ( ( ( ( ( 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 ) )
89 88 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 ) )
90 brxp 
 |-  ( z ( Y X. Y ) w <-> ( z e. Y /\ w e. Y ) )
91 90 simplbi 
 |-  ( z ( Y X. Y ) w -> z e. Y )
92 89 91 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 ) )
93 82 92 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 ) )
94 69 93 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 )
95 32 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 )
96 weso 
 |-  ( ( W ` X ) We X -> ( W ` X ) Or X )
97 95 96 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 )
98 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 )
99 98 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 )
100 sotric 
 |-  ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> -. ( w = z \/ z ( W ` X ) w ) ) )
101 ioran 
 |-  ( -. ( w = z \/ z ( W ` X ) w ) <-> ( -. w = z /\ -. z ( W ` X ) w ) )
102 100 101 bitrdi 
 |-  ( ( ( W ` X ) Or X /\ ( w e. X /\ z e. X ) ) -> ( w ( W ` X ) z <-> ( -. w = z /\ -. z ( W ` X ) w ) ) )
103 97 99 75 102 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 ) ) )
104 68 94 103 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 )
105 104 45 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 } ) )
106 105 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 } ) ) )
107 106 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 } ) )
108 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 )
109 107 108 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 } ) )
110 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 ) )
111 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 ) ) )
112 111 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 ) ) )
113 87 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 ) )
114 df-ss 
 |-  ( R C_ ( Y X. Y ) <-> ( R i^i ( Y X. Y ) ) = R )
115 113 114 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 )
116 112 115 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 )
117 inss2 
 |-  ( ( W ` X ) i^i ( Y X. Y ) ) C_ ( Y X. Y )
118 xpss1 
 |-  ( Y C_ X -> ( Y X. Y ) C_ ( X X. Y ) )
119 98 118 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 ) )
120 117 119 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 ) )
121 df-ss 
 |-  ( ( ( 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 ) ) )
122 120 121 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 ) ) )
123 110 116 122 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 ) ) )
124 109 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 } ) ) )
125 124 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 } ) ) ) )
126 123 125 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 } ) ) ) )
127 109 126 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 } ) ) ) ) )
128 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 )
129 22 adantr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W ( W ` X ) )
130 129 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 ) )
131 1 128 130 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 )
132 74 131 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 )
133 127 132 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 )
134 133 63 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 )
135 134 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 ) )
136 61 135 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 ) )
137 38 136 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 ) )
138 137 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 ) = (/) ) )
139 16 138 mpd 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> ( X \ Y ) = (/) )
140 ssdif0 
 |-  ( X C_ Y <-> ( X \ Y ) = (/) )
141 139 140 sylibr 
 |-  ( ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) /\ ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) ) -> X C_ Y )
142 141 ex 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( ( Y C_ X /\ R = ( ( W ` X ) i^i ( X X. Y ) ) ) -> X C_ Y ) )
143 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 )
144 simprl 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y W R )
145 1 17 143 129 144 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 ) ) ) ) )
146 15 142 145 mpjaod 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X C_ Y )
147 13 146 eqssd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Y = X )
148 6 adantr 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> Fun W )
149 147 144 eqbrtrrd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> X W R )
150 funbrfv 
 |-  ( Fun W -> ( X W R -> ( W ` X ) = R ) )
151 148 149 150 sylc 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( W ` X ) = R )
152 151 eqcomd 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> R = ( W ` X ) )
153 147 152 jca 
 |-  ( ( ph /\ ( Y W R /\ ( Y F R ) e. Y ) ) -> ( Y = X /\ R = ( W ` X ) ) )
154 153 ex 
 |-  ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) -> ( Y = X /\ R = ( W ` X ) ) ) )
155 1 2 3 4 fpwwe2lem12 
 |-  ( ph -> ( X F ( W ` X ) ) e. X )
156 22 155 jca 
 |-  ( ph -> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) )
157 breq12 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R <-> X W ( W ` X ) ) )
158 oveq12 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( Y F R ) = ( X F ( W ` X ) ) )
159 simpl 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> Y = X )
160 158 159 eleq12d 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y F R ) e. Y <-> ( X F ( W ` X ) ) e. X ) )
161 157 160 anbi12d 
 |-  ( ( Y = X /\ R = ( W ` X ) ) -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( X W ( W ` X ) /\ ( X F ( W ` X ) ) e. X ) ) )
162 156 161 syl5ibrcom 
 |-  ( ph -> ( ( Y = X /\ R = ( W ` X ) ) -> ( Y W R /\ ( Y F R ) e. Y ) ) )
163 154 162 impbid 
 |-  ( ph -> ( ( Y W R /\ ( Y F R ) e. Y ) <-> ( Y = X /\ R = ( W ` X ) ) ) )