Metamath Proof Explorer

Theorem fpwwe2lem12

Description: Lemma for fpwwe2 . (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 fpwwe2lem12 
|- ( ph -> ( X F ( W ` X ) ) e. 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 ssun2 
 |-  { ( X F ( W ` X ) ) } C_ ( X u. { ( X F ( W ` X ) ) } )
6 2 adantr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> A e. V )
7 3 adantlr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ A /\ r C_ ( x X. x ) /\ r We x ) ) -> ( x F r ) e. A )
8 1 6 7 4 fpwwe2lem11 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> X e. dom W )
9 1 6 7 4 fpwwe2lem10 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> W : dom W --> ~P ( X X. X ) )
10 ffun 
 |-  ( W : dom W --> ~P ( X X. X ) -> Fun W )
11 funfvbrb 
 |-  ( Fun W -> ( X e. dom W <-> X W ( W ` X ) ) )
12 9 10 11 3syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X e. dom W <-> X W ( W ` X ) ) )
13 8 12 mpbid 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> X W ( W ` X ) )
14 1 6 fpwwe2lem2 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( 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 ) ) ) )
15 13 14 mpbid 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. 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 ) ) )
16 15 simpld 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X C_ A /\ ( W ` X ) C_ ( X X. X ) ) )
17 16 simpld 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> X C_ A )
18 16 simprd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) C_ ( X X. X ) )
19 15 simprd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) We X /\ A. y e. X [. ( `' ( W ` X ) " { y } ) / u ]. ( u F ( ( W ` X ) i^i ( u X. u ) ) ) = y ) )
20 19 simpld 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) We X )
21 17 18 20 3jca 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X C_ A /\ ( W ` X ) C_ ( X X. X ) /\ ( W ` X ) We X ) )
22 1 2 3 fpwwe2lem4 
 |-  ( ( ph /\ ( X C_ A /\ ( W ` X ) C_ ( X X. X ) /\ ( W ` X ) We X ) ) -> ( X F ( W ` X ) ) e. A )
23 21 22 syldan 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X F ( W ` X ) ) e. A )
24 23 snssd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> { ( X F ( W ` X ) ) } C_ A )
25 17 24 unssd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) C_ A )
26 ssun1 
 |-  X C_ ( X u. { ( X F ( W ` X ) ) } )
27 xpss12 
 |-  ( ( X C_ ( X u. { ( X F ( W ` X ) ) } ) /\ X C_ ( X u. { ( X F ( W ` X ) ) } ) ) -> ( X X. X ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) )
28 26 26 27 mp2an 
 |-  ( X X. X ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) )
29 18 28 sstrdi 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) )
30 xpss12 
 |-  ( ( X C_ ( X u. { ( X F ( W ` X ) ) } ) /\ { ( X F ( W ` X ) ) } C_ ( X u. { ( X F ( W ` X ) ) } ) ) -> ( X X. { ( X F ( W ` X ) ) } ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) )
31 26 5 30 mp2an 
 |-  ( X X. { ( X F ( W ` X ) ) } ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) )
32 31 a1i 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X X. { ( X F ( W ` X ) ) } ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) )
33 29 32 unssd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) )
34 25 33 jca 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( X u. { ( X F ( W ` X ) ) } ) C_ A /\ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) ) )
35 ssdif0 
 |-  ( x C_ { ( X F ( W ` X ) ) } <-> ( x \ { ( X F ( W ` X ) ) } ) = (/) )
36 simpllr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> -. ( X F ( W ` X ) ) e. X )
37 18 ad2antrr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( W ` X ) C_ ( X X. X ) )
38 37 ssbrd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) -> ( X F ( W ` X ) ) ( X X. X ) ( X F ( W ` X ) ) ) )
39 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) ( X F ( W ` X ) ) <-> ( ( X F ( W ` X ) ) e. X /\ ( X F ( W ` X ) ) e. X ) )
40 39 simplbi 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) ( X F ( W ` X ) ) -> ( X F ( W ` X ) ) e. X )
41 38 40 syl6 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) -> ( X F ( W ` X ) ) e. X ) )
42 36 41 mtod 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> -. ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) )
43 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) <-> ( ( X F ( W ` X ) ) e. X /\ ( X F ( W ` X ) ) e. { ( X F ( W ` X ) ) } ) )
44 43 simplbi 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) -> ( X F ( W ` X ) ) e. X )
45 36 44 nsyl 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) )
46 ovex 
 |-  ( X F ( W ` X ) ) e. _V
47 breq2 
 |-  ( y = ( X F ( W ` X ) ) -> ( ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) ( X F ( W ` X ) ) ) )
48 brun 
 |-  ( ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) ( X F ( W ` X ) ) <-> ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) )
49 47 48 bitrdi 
 |-  ( y = ( X F ( W ` X ) ) -> ( ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) ) )
50 49 notbid 
 |-  ( y = ( X F ( W ` X ) ) -> ( -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) ) )
51 46 50 rexsn 
 |-  ( E. y e. { ( X F ( W ` X ) ) } -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) )
52 ioran 
 |-  ( -. ( ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) <-> ( -. ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) /\ -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) )
53 51 52 bitri 
 |-  ( E. y e. { ( X F ( W ` X ) ) } -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( -. ( X F ( W ` X ) ) ( W ` X ) ( X F ( W ` X ) ) /\ -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) ( X F ( W ` X ) ) ) )
54 42 45 53 sylanbrc 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> E. y e. { ( X F ( W ` X ) ) } -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
55 simpr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> x C_ { ( X F ( W ` X ) ) } )
56 sssn 
 |-  ( x C_ { ( X F ( W ` X ) ) } <-> ( x = (/) \/ x = { ( X F ( W ` X ) ) } ) )
57 55 56 sylib 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( x = (/) \/ x = { ( X F ( W ` X ) ) } ) )
58 simplrr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> x =/= (/) )
59 58 neneqd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> -. x = (/) )
60 57 59 orcnd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> x = { ( X F ( W ` X ) ) } )
61 60 raleqdv 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
62 breq1 
 |-  ( z = ( X F ( W ` X ) ) -> ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
63 62 notbid 
 |-  ( z = ( X F ( W ` X ) ) -> ( -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
64 46 63 ralsn 
 |-  ( A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
65 61 64 bitrdi 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
66 60 65 rexeqbidv 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> ( E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> E. y e. { ( X F ( W ` X ) ) } -. ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
67 54 66 mpbird 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
68 67 ex 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) -> ( x C_ { ( X F ( W ` X ) ) } -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
69 35 68 syl5bir 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) -> ( ( x \ { ( X F ( W ` X ) ) } ) = (/) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
70 vex 
 |-  x e. _V
71 difexg 
 |-  ( x e. _V -> ( x \ { ( X F ( W ` X ) ) } ) e. _V )
72 70 71 mp1i 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( x \ { ( X F ( W ` X ) ) } ) e. _V )
73 wefr 
 |-  ( ( W ` X ) We X -> ( W ` X ) Fr X )
74 20 73 syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) Fr X )
75 74 ad2antrr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( W ` X ) Fr X )
76 simplrl 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> x C_ ( X u. { ( X F ( W ` X ) ) } ) )
77 uncom 
 |-  ( X u. { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } u. X )
78 76 77 sseqtrdi 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> x C_ ( { ( X F ( W ` X ) ) } u. X ) )
79 ssundif 
 |-  ( x C_ ( { ( X F ( W ` X ) ) } u. X ) <-> ( x \ { ( X F ( W ` X ) ) } ) C_ X )
80 78 79 sylib 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( x \ { ( X F ( W ` X ) ) } ) C_ X )
81 simpr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( x \ { ( X F ( W ` X ) ) } ) =/= (/) )
82 fri 
 |-  ( ( ( ( x \ { ( X F ( W ` X ) ) } ) e. _V /\ ( W ` X ) Fr X ) /\ ( ( x \ { ( X F ( W ` X ) ) } ) C_ X /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) ) -> E. y e. ( x \ { ( X F ( W ` X ) ) } ) A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y )
83 72 75 80 81 82 syl22anc 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> E. y e. ( x \ { ( X F ( W ` X ) ) } ) A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y )
84 brun 
 |-  ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( z ( W ` X ) y \/ z ( X X. { ( X F ( W ` X ) ) } ) y ) )
85 idd 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( z ( W ` X ) y -> z ( W ` X ) y ) )
86 brxp 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y <-> ( z e. X /\ y e. { ( X F ( W ` X ) ) } ) )
87 86 simprbi 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y -> y e. { ( X F ( W ` X ) ) } )
88 eldifn 
 |-  ( y e. ( x \ { ( X F ( W ` X ) ) } ) -> -. y e. { ( X F ( W ` X ) ) } )
89 88 adantl 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> -. y e. { ( X F ( W ` X ) ) } )
90 89 pm2.21d 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( y e. { ( X F ( W ` X ) ) } -> z ( W ` X ) y ) )
91 87 90 syl5 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( z ( X X. { ( X F ( W ` X ) ) } ) y -> z ( W ` X ) y ) )
92 85 91 jaod 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( ( z ( W ` X ) y \/ z ( X X. { ( X F ( W ` X ) ) } ) y ) -> z ( W ` X ) y ) )
93 84 92 syl5bi 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y -> z ( W ` X ) y ) )
94 93 con3d 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( -. z ( W ` X ) y -> -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
95 94 ralimdv 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y -> A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
96 simpr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> -. ( X F ( W ` X ) ) e. X )
97 96 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> -. ( X F ( W ` X ) ) e. X )
98 18 ad3antrrr 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( W ` X ) C_ ( X X. X ) )
99 98 ssbrd 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( ( X F ( W ` X ) ) ( W ` X ) y -> ( X F ( W ` X ) ) ( X X. X ) y ) )
100 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) y <-> ( ( X F ( W ` X ) ) e. X /\ y e. X ) )
101 100 simplbi 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) y -> ( X F ( W ` X ) ) e. X )
102 99 101 syl6 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( ( X F ( W ` X ) ) ( W ` X ) y -> ( X F ( W ` X ) ) e. X ) )
103 97 102 mtod 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> -. ( X F ( W ` X ) ) ( W ` X ) y )
104 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y <-> ( ( X F ( W ` X ) ) e. X /\ y e. { ( X F ( W ` X ) ) } ) )
105 104 simprbi 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y -> y e. { ( X F ( W ` X ) ) } )
106 89 105 nsyl 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y )
107 brun 
 |-  ( ( X F ( W ` X ) ) ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( ( X F ( W ` X ) ) ( W ` X ) y \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) )
108 62 107 bitrdi 
 |-  ( z = ( X F ( W ` X ) ) -> ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( ( X F ( W ` X ) ) ( W ` X ) y \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) ) )
109 108 notbid 
 |-  ( z = ( X F ( W ` X ) ) -> ( -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( ( X F ( W ` X ) ) ( W ` X ) y \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) ) )
110 46 109 ralsn 
 |-  ( A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> -. ( ( X F ( W ` X ) ) ( W ` X ) y \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) )
111 ioran 
 |-  ( -. ( ( X F ( W ` X ) ) ( W ` X ) y \/ ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) <-> ( -. ( X F ( W ` X ) ) ( W ` X ) y /\ -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) )
112 110 111 bitri 
 |-  ( A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( -. ( X F ( W ` X ) ) ( W ` X ) y /\ -. ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y ) )
113 103 106 112 sylanbrc 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
114 95 113 jctird 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y -> ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y /\ A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) ) )
115 ssun1 
 |-  x C_ ( x u. { ( X F ( W ` X ) ) } )
116 undif1 
 |-  ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } ) = ( x u. { ( X F ( W ` X ) ) } )
117 115 116 sseqtrri 
 |-  x C_ ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } )
118 ralun 
 |-  ( ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y /\ A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) -> A. z e. ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
119 ssralv 
 |-  ( x C_ ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } ) -> ( A. z e. ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y -> A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
120 117 118 119 mpsyl 
 |-  ( ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y /\ A. z e. { ( X F ( W ` X ) ) } -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) -> A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
121 114 120 syl6 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y -> A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
122 eldifi 
 |-  ( y e. ( x \ { ( X F ( W ` X ) ) } ) -> y e. x )
123 122 adantl 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> y e. x )
124 121 123 jctild 
 |-  ( ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) /\ y e. ( x \ { ( X F ( W ` X ) ) } ) ) -> ( A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y -> ( y e. x /\ A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) ) )
125 124 expimpd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( ( y e. ( x \ { ( X F ( W ` X ) ) } ) /\ A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y ) -> ( y e. x /\ A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) ) )
126 125 reximdv2 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> ( E. y e. ( x \ { ( X F ( W ` X ) ) } ) A. z e. ( x \ { ( X F ( W ` X ) ) } ) -. z ( W ` X ) y -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
127 83 126 mpd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ ( x \ { ( X F ( W ` X ) ) } ) =/= (/) ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
128 127 ex 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) -> ( ( x \ { ( X F ( W ` X ) ) } ) =/= (/) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
129 69 128 pm2.61dne 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
130 129 ex 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
131 130 alrimiv 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> A. x ( ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
132 df-fr 
 |-  ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) Fr ( X u. { ( X F ( W ` X ) ) } ) <-> A. x ( ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) -> E. y e. x A. z e. x -. z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
133 131 132 sylibr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) Fr ( X u. { ( X F ( W ` X ) ) } ) )
134 elun 
 |-  ( x e. ( X u. { ( X F ( W ` X ) ) } ) <-> ( x e. X \/ x e. { ( X F ( W ` X ) ) } ) )
135 elun 
 |-  ( y e. ( X u. { ( X F ( W ` X ) ) } ) <-> ( y e. X \/ y e. { ( X F ( W ` X ) ) } ) )
136 134 135 anbi12i 
 |-  ( ( x e. ( X u. { ( X F ( W ` X ) ) } ) /\ y e. ( X u. { ( X F ( W ` X ) ) } ) ) <-> ( ( x e. X \/ x e. { ( X F ( W ` X ) ) } ) /\ ( y e. X \/ y e. { ( X F ( W ` X ) ) } ) ) )
137 weso 
 |-  ( ( W ` X ) We X -> ( W ` X ) Or X )
138 20 137 syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) Or X )
139 solin 
 |-  ( ( ( W ` X ) Or X /\ ( x e. X /\ y e. X ) ) -> ( x ( W ` X ) y \/ x = y \/ y ( W ` X ) x ) )
140 138 139 sylan 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x ( W ` X ) y \/ x = y \/ y ( W ` X ) x ) )
141 ssun1 
 |-  ( W ` X ) C_ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
142 141 a1i 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( W ` X ) C_ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) )
143 142 ssbrd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x ( W ` X ) y -> x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
144 idd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x = y -> x = y ) )
145 142 ssbrd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( y ( W ` X ) x -> y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
146 143 144 145 3orim123d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( W ` X ) y \/ x = y \/ y ( W ` X ) x ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
147 140 146 mpd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
148 147 ex 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x e. X /\ y e. X ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
149 simpr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) ) -> ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) )
150 149 ancomd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) ) -> ( y e. X /\ x e. { ( X F ( W ` X ) ) } ) )
151 brxp 
 |-  ( y ( X X. { ( X F ( W ` X ) ) } ) x <-> ( y e. X /\ x e. { ( X F ( W ` X ) ) } ) )
152 150 151 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) ) -> y ( X X. { ( X F ( W ` X ) ) } ) x )
153 ssun2 
 |-  ( X X. { ( X F ( W ` X ) ) } ) C_ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
154 153 ssbri 
 |-  ( y ( X X. { ( X F ( W ` X ) ) } ) x -> y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x )
155 3mix3 
 |-  ( y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
156 152 154 155 3syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
157 156 ex 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x e. { ( X F ( W ` X ) ) } /\ y e. X ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
158 simpr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) ) -> ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) )
159 brxp 
 |-  ( x ( X X. { ( X F ( W ` X ) ) } ) y <-> ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) )
160 158 159 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) ) -> x ( X X. { ( X F ( W ` X ) ) } ) y )
161 153 ssbri 
 |-  ( x ( X X. { ( X F ( W ` X ) ) } ) y -> x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
162 3mix1 
 |-  ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
163 160 161 162 3syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
164 163 ex 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
165 elsni 
 |-  ( x e. { ( X F ( W ` X ) ) } -> x = ( X F ( W ` X ) ) )
166 elsni 
 |-  ( y e. { ( X F ( W ` X ) ) } -> y = ( X F ( W ` X ) ) )
167 eqtr3 
 |-  ( ( x = ( X F ( W ` X ) ) /\ y = ( X F ( W ` X ) ) ) -> x = y )
168 165 166 167 syl2an 
 |-  ( ( x e. { ( X F ( W ` X ) ) } /\ y e. { ( X F ( W ` X ) ) } ) -> x = y )
169 168 3mix2d 
 |-  ( ( x e. { ( X F ( W ` X ) ) } /\ y e. { ( X F ( W ` X ) ) } ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
170 169 a1i 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x e. { ( X F ( W ` X ) ) } /\ y e. { ( X F ( W ` X ) ) } ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
171 148 157 164 170 ccased 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( ( x e. X \/ x e. { ( X F ( W ` X ) ) } ) /\ ( y e. X \/ y e. { ( X F ( W ` X ) ) } ) ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
172 136 171 syl5bi 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( x e. ( X u. { ( X F ( W ` X ) ) } ) /\ y e. ( X u. { ( X F ( W ` X ) ) } ) ) -> ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
173 172 ralrimivv 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> A. x e. ( X u. { ( X F ( W ` X ) ) } ) A. y e. ( X u. { ( X F ( W ` X ) ) } ) ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) )
174 dfwe2 
 |-  ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) <-> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) Fr ( X u. { ( X F ( W ` X ) ) } ) /\ A. x e. ( X u. { ( X F ( W ` X ) ) } ) A. y e. ( X u. { ( X F ( W ` X ) ) } ) ( x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y \/ x = y \/ y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x ) ) )
175 133 173 174 sylanbrc 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) )
176 1 fpwwe2cbv 
 |-  W = { <. a , s >. | ( ( a C_ A /\ s C_ ( a X. a ) ) /\ ( s We a /\ A. z e. a [. ( `' s " { z } ) / b ]. ( b F ( s i^i ( b X. b ) ) ) = z ) ) }
177 176 6 13 fpwwe2lem3 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( `' ( W ` X ) " { y } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) ) = y )
178 cnvimass 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) C_ dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
179 fvex 
 |-  ( W ` X ) e. _V
180 snex 
 |-  { ( X F ( W ` X ) ) } e. _V
181 xpexg 
 |-  ( ( X e. dom W /\ { ( X F ( W ` X ) ) } e. _V ) -> ( X X. { ( X F ( W ` X ) ) } ) e. _V )
182 8 180 181 sylancl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X X. { ( X F ( W ` X ) ) } ) e. _V )
183 unexg 
 |-  ( ( ( W ` X ) e. _V /\ ( X X. { ( X F ( W ` X ) ) } ) e. _V ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
184 179 182 183 sylancr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
185 184 dmexd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
186 ssexg 
 |-  ( ( ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) C_ dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) /\ dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
187 178 185 186 sylancr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
188 187 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
189 id 
 |-  ( u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) -> u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) )
190 simpr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> y e. X )
191 simplr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> -. ( X F ( W ` X ) ) e. X )
192 nelne2 
 |-  ( ( y e. X /\ -. ( X F ( W ` X ) ) e. X ) -> y =/= ( X F ( W ` X ) ) )
193 190 191 192 syl2anc 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> y =/= ( X F ( W ` X ) ) )
194 87 166 syl 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y -> y = ( X F ( W ` X ) ) )
195 194 necon3ai 
 |-  ( y =/= ( X F ( W ` X ) ) -> -. z ( X X. { ( X F ( W ` X ) ) } ) y )
196 biorf 
 |-  ( -. z ( X X. { ( X F ( W ` X ) ) } ) y -> ( z ( W ` X ) y <-> ( z ( X X. { ( X F ( W ` X ) ) } ) y \/ z ( W ` X ) y ) ) )
197 193 195 196 3syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( z ( W ` X ) y <-> ( z ( X X. { ( X F ( W ` X ) ) } ) y \/ z ( W ` X ) y ) ) )
198 orcom 
 |-  ( ( z ( X X. { ( X F ( W ` X ) ) } ) y \/ z ( W ` X ) y ) <-> ( z ( W ` X ) y \/ z ( X X. { ( X F ( W ` X ) ) } ) y ) )
199 198 84 bitr4i 
 |-  ( ( z ( X X. { ( X F ( W ` X ) ) } ) y \/ z ( W ` X ) y ) <-> z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
200 197 199 bitr2di 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> z ( W ` X ) y ) )
201 vex 
 |-  z e. _V
202 201 eliniseg 
 |-  ( y e. _V -> ( z e. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) <-> z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y ) )
203 202 elv 
 |-  ( z e. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) <-> z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
204 201 eliniseg 
 |-  ( y e. _V -> ( z e. ( `' ( W ` X ) " { y } ) <-> z ( W ` X ) y ) )
205 204 elv 
 |-  ( z e. ( `' ( W ` X ) " { y } ) <-> z ( W ` X ) y )
206 200 203 205 3bitr4g 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( z e. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) <-> z e. ( `' ( W ` X ) " { y } ) ) )
207 206 eqrdv 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( `' ( W ` X ) " { y } ) )
208 189 207 sylan9eqr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> u = ( `' ( W ` X ) " { y } ) )
209 208 sqxpeqd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( u X. u ) = ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) )
210 209 ineq2d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) = ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) )
211 indir 
 |-  ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) )
212 inxp 
 |-  ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) )
213 incom 
 |-  ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) = ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } )
214 cnvimass 
 |-  ( `' ( W ` X ) " { y } ) C_ dom ( W ` X )
215 18 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( W ` X ) C_ ( X X. X ) )
216 dmss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
217 215 216 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
218 dmxpid 
 |-  dom ( X X. X ) = X
219 217 218 sseqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> dom ( W ` X ) C_ X )
220 214 219 sstrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( W ` X ) " { y } ) C_ X )
221 220 191 ssneldd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> -. ( X F ( W ` X ) ) e. ( `' ( W ` X ) " { y } ) )
222 disjsn 
 |-  ( ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } ) = (/) <-> -. ( X F ( W ` X ) ) e. ( `' ( W ` X ) " { y } ) )
223 221 222 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } ) = (/) )
224 213 223 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) = (/) )
225 224 xpeq2d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) ) = ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. (/) ) )
226 xp0 
 |-  ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. (/) ) = (/)
227 225 226 eqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) ) = (/) )
228 212 227 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = (/) )
229 228 uneq2d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) ) = ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. (/) ) )
230 211 229 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. (/) ) )
231 un0 
 |-  ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. (/) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) )
232 230 231 eqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) )
233 232 adantr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) )
234 210 233 eqtrd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) )
235 208 234 oveq12d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = ( ( `' ( W ` X ) " { y } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) ) )
236 235 eqeq1d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y <-> ( ( `' ( W ` X ) " { y } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) ) = y ) )
237 188 236 sbcied 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y <-> ( ( `' ( W ` X ) " { y } ) F ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) ) = y ) )
238 177 237 mpbird 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y )
239 166 adantl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> y = ( X F ( W ` X ) ) )
240 239 eqcomd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( X F ( W ` X ) ) = y )
241 187 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
242 simplr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> -. ( X F ( W ` X ) ) e. X )
243 239 eleq1d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( y e. dom `' ( W ` X ) <-> ( X F ( W ` X ) ) e. dom `' ( W ` X ) ) )
244 18 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( W ` X ) C_ ( X X. X ) )
245 rnss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> ran ( W ` X ) C_ ran ( X X. X ) )
246 244 245 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ran ( W ` X ) C_ ran ( X X. X ) )
247 df-rn 
 |-  ran ( W ` X ) = dom `' ( W ` X )
248 rnxpid 
 |-  ran ( X X. X ) = X
249 246 247 248 3sstr3g 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> dom `' ( W ` X ) C_ X )
250 249 sseld 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( X F ( W ` X ) ) e. dom `' ( W ` X ) -> ( X F ( W ` X ) ) e. X ) )
251 243 250 sylbid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( y e. dom `' ( W ` X ) -> ( X F ( W ` X ) ) e. X ) )
252 242 251 mtod 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> -. y e. dom `' ( W ` X ) )
253 ndmima 
 |-  ( -. y e. dom `' ( W ` X ) -> ( `' ( W ` X ) " { y } ) = (/) )
254 252 253 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( W ` X ) " { y } ) = (/) )
255 239 sneqd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> { y } = { ( X F ( W ` X ) ) } )
256 255 imaeq2d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) = ( `' ( X X. { ( X F ( W ` X ) ) } ) " { ( X F ( W ` X ) ) } ) )
257 df-ima 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) " { ( X F ( W ` X ) ) } ) = ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } )
258 cnvxp 
 |-  `' ( X X. { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
259 258 reseq1i 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ( ( { ( X F ( W ` X ) ) } X. X ) |` { ( X F ( W ` X ) ) } )
260 ssid 
 |-  { ( X F ( W ` X ) ) } C_ { ( X F ( W ` X ) ) }
261 xpssres 
 |-  ( { ( X F ( W ` X ) ) } C_ { ( X F ( W ` X ) ) } -> ( ( { ( X F ( W ` X ) ) } X. X ) |` { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X ) )
262 260 261 ax-mp 
 |-  ( ( { ( X F ( W ` X ) ) } X. X ) |` { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
263 259 262 eqtri 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
264 263 rneqi 
 |-  ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ran ( { ( X F ( W ` X ) ) } X. X )
265 46 snnz 
 |-  { ( X F ( W ` X ) ) } =/= (/)
266 rnxp 
 |-  ( { ( X F ( W ` X ) ) } =/= (/) -> ran ( { ( X F ( W ` X ) ) } X. X ) = X )
267 265 266 ax-mp 
 |-  ran ( { ( X F ( W ` X ) ) } X. X ) = X
268 264 267 eqtri 
 |-  ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = X
269 257 268 eqtri 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) " { ( X F ( W ` X ) ) } ) = X
270 256 269 eqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) = X )
271 254 270 uneq12d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( `' ( W ` X ) " { y } ) u. ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) ) = ( (/) u. X ) )
272 cnvun 
 |-  `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) = ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) )
273 272 imaeq1i 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) ) " { y } )
274 imaundir 
 |-  ( ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) " { y } ) u. ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) )
275 273 274 eqtri 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) " { y } ) u. ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) )
276 un0 
 |-  ( X u. (/) ) = X
277 uncom 
 |-  ( X u. (/) ) = ( (/) u. X )
278 276 277 eqtr3i 
 |-  X = ( (/) u. X )
279 271 275 278 3eqtr4g 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = X )
280 189 279 sylan9eqr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> u = X )
281 280 sqxpeqd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( u X. u ) = ( X X. X ) )
282 281 ineq2d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) = ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( X X. X ) ) )
283 indir 
 |-  ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( X X. X ) ) = ( ( ( W ` X ) i^i ( X X. X ) ) u. ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( X X. X ) ) )
284 df-ss 
 |-  ( ( W ` X ) C_ ( X X. X ) <-> ( ( W ` X ) i^i ( X X. X ) ) = ( W ` X ) )
285 244 284 sylib 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( W ` X ) i^i ( X X. X ) ) = ( W ` X ) )
286 incom 
 |-  ( { ( X F ( W ` X ) ) } i^i X ) = ( X i^i { ( X F ( W ` X ) ) } )
287 disjsn 
 |-  ( ( X i^i { ( X F ( W ` X ) ) } ) = (/) <-> -. ( X F ( W ` X ) ) e. X )
288 242 287 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( X i^i { ( X F ( W ` X ) ) } ) = (/) )
289 286 288 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( { ( X F ( W ` X ) ) } i^i X ) = (/) )
290 289 xpeq2d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( X X. ( { ( X F ( W ` X ) ) } i^i X ) ) = ( X X. (/) ) )
291 xpindi 
 |-  ( X X. ( { ( X F ( W ` X ) ) } i^i X ) ) = ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( X X. X ) )
292 xp0 
 |-  ( X X. (/) ) = (/)
293 290 291 292 3eqtr3g 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( X X. X ) ) = (/) )
294 285 293 uneq12d 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( ( W ` X ) i^i ( X X. X ) ) u. ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( X X. X ) ) ) = ( ( W ` X ) u. (/) ) )
295 283 294 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( X X. X ) ) = ( ( W ` X ) u. (/) ) )
296 un0 
 |-  ( ( W ` X ) u. (/) ) = ( W ` X )
297 295 296 eqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( X X. X ) ) = ( W ` X ) )
298 297 adantr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( X X. X ) ) = ( W ` X ) )
299 282 298 eqtrd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) = ( W ` X ) )
300 280 299 oveq12d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = ( X F ( W ` X ) ) )
301 300 eqeq1d 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) /\ u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) ) -> ( ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y <-> ( X F ( W ` X ) ) = y ) )
302 241 301 sbcied 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y <-> ( X F ( W ` X ) ) = y ) )
303 240 302 mpbird 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y )
304 238 303 jaodan 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( y e. X \/ y e. { ( X F ( W ` X ) ) } ) ) -> [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y )
305 135 304 sylan2b 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. ( X u. { ( X F ( W ` X ) ) } ) ) -> [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y )
306 305 ralrimiva 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> A. y e. ( X u. { ( X F ( W ` X ) ) } ) [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y )
307 175 306 jca 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) /\ A. y e. ( X u. { ( X F ( W ` X ) ) } ) [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y ) )
308 1 2 fpwwe2lem2 
 |-  ( ph -> ( ( X u. { ( X F ( W ` X ) ) } ) W ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) <-> ( ( ( X u. { ( X F ( W ` X ) ) } ) C_ A /\ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) ) /\ ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) /\ A. y e. ( X u. { ( X F ( W ` X ) ) } ) [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y ) ) ) )
309 308 adantr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( X u. { ( X F ( W ` X ) ) } ) W ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) <-> ( ( ( X u. { ( X F ( W ` X ) ) } ) C_ A /\ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) C_ ( ( X u. { ( X F ( W ` X ) ) } ) X. ( X u. { ( X F ( W ` X ) ) } ) ) ) /\ ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) /\ A. y e. ( X u. { ( X F ( W ` X ) ) } ) [. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) / u ]. ( u F ( ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) i^i ( u X. u ) ) ) = y ) ) ) )
310 34 307 309 mpbir2and 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) W ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) )
311 1 relopabiv 
 |-  Rel W
312 311 releldmi 
 |-  ( ( X u. { ( X F ( W ` X ) ) } ) W ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) -> ( X u. { ( X F ( W ` X ) ) } ) e. dom W )
313 elssuni 
 |-  ( ( X u. { ( X F ( W ` X ) ) } ) e. dom W -> ( X u. { ( X F ( W ` X ) ) } ) C_ U. dom W )
314 310 312 313 3syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) C_ U. dom W )
315 314 4 sseqtrrdi 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) C_ X )
316 5 315 sstrid 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> { ( X F ( W ` X ) ) } C_ X )
317 46 snss 
 |-  ( ( X F ( W ` X ) ) e. X <-> { ( X F ( W ` X ) ) } C_ X )
318 316 317 sylibr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X F ( W ` X ) ) e. X )
319 318 pm2.18da 
 |-  ( ph -> ( X F ( W ` X ) ) e. X )