This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 sssn 
 |-  ( x C_ { ( X F ( W ` X ) ) } <-> ( x = (/) \/ x = { ( X F ( W ` X ) ) } ) )
56 55 bilani 
 |-  ( ( ( ( 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 ) ) } ) )
57 simplrr 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> x =/= (/) )
58 57 neneqd 
 |-  ( ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x C_ ( X u. { ( X F ( W ` X ) ) } ) /\ x =/= (/) ) ) /\ x C_ { ( X F ( W ` X ) ) } ) -> -. x = (/) )
59 56 58 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 ) ) } )
60 59 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 ) )
61 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 ) )
62 61 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 ) )
63 46 62 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 )
64 60 63 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 ) )
65 59 64 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 ) )
66 54 65 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 )
67 66 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 ) )
68 35 67 biimtrrid 
 |-  ( ( ( 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 ) )
69 vex 
 |-  x e. _V
70 difexg 
 |-  ( x e. _V -> ( x \ { ( X F ( W ` X ) ) } ) e. _V )
71 69 70 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 )
72 wefr 
 |-  ( ( W ` X ) We X -> ( W ` X ) Fr X )
73 20 72 syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) Fr X )
74 73 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 )
75 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 ) ) } ) )
76 uncom 
 |-  ( X u. { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } u. X )
77 75 76 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 ) )
78 ssundif 
 |-  ( x C_ ( { ( X F ( W ` X ) ) } u. X ) <-> ( x \ { ( X F ( W ` X ) ) } ) C_ X )
79 77 78 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 )
80 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 ) ) } ) =/= (/) )
81 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 )
82 71 74 79 80 81 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 )
83 brun 
 |-  ( z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y <-> ( z ( W ` X ) y \/ z ( X X. { ( X F ( W ` X ) ) } ) y ) )
84 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 ) )
85 brxp 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y <-> ( z e. X /\ y e. { ( X F ( W ` X ) ) } ) )
86 85 simprbi 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y -> y e. { ( X F ( W ` X ) ) } )
87 eldifn 
 |-  ( y e. ( x \ { ( X F ( W ` X ) ) } ) -> -. y e. { ( X F ( W ` X ) ) } )
88 87 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 ) ) } )
89 88 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 ) )
90 86 89 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 ) )
91 84 90 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 ) )
92 83 91 biimtrid 
 |-  ( ( ( ( ( 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 ) )
93 92 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 ) )
94 93 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 ) )
95 simpr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> -. ( X F ( W ` X ) ) e. X )
96 95 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 )
97 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 ) )
98 97 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 ) )
99 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) y <-> ( ( X F ( W ` X ) ) e. X /\ y e. X ) )
100 99 simplbi 
 |-  ( ( X F ( W ` X ) ) ( X X. X ) y -> ( X F ( W ` X ) ) e. X )
101 98 100 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 ) )
102 96 101 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 )
103 brxp 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y <-> ( ( X F ( W ` X ) ) e. X /\ y e. { ( X F ( W ` X ) ) } ) )
104 103 simprbi 
 |-  ( ( X F ( W ` X ) ) ( X X. { ( X F ( W ` X ) ) } ) y -> y e. { ( X F ( W ` X ) ) } )
105 88 104 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 )
106 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 ) )
107 61 106 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 ) ) )
108 107 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 ) ) )
109 46 108 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 ) )
110 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 ) )
111 109 110 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 ) )
112 102 105 111 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 )
113 94 112 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 ) ) )
114 ssun1 
 |-  x C_ ( x u. { ( X F ( W ` X ) ) } )
115 undif1 
 |-  ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } ) = ( x u. { ( X F ( W ` X ) ) } )
116 114 115 sseqtrri 
 |-  x C_ ( ( x \ { ( X F ( W ` X ) ) } ) u. { ( X F ( W ` X ) ) } )
117 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 )
118 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 ) )
119 116 117 118 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 )
120 113 119 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 ) )
121 eldifi 
 |-  ( y e. ( x \ { ( X F ( W ` X ) ) } ) -> y e. x )
122 121 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 )
123 120 122 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 ) ) )
124 123 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 ) ) )
125 124 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 ) )
126 82 125 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 )
127 126 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 ) )
128 68 127 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 )
129 128 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 ) )
130 129 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 ) )
131 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 ) )
132 130 131 sylibr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) Fr ( X u. { ( X F ( W ` X ) ) } ) )
133 elun 
 |-  ( x e. ( X u. { ( X F ( W ` X ) ) } ) <-> ( x e. X \/ x e. { ( X F ( W ` X ) ) } ) )
134 elun 
 |-  ( y e. ( X u. { ( X F ( W ` X ) ) } ) <-> ( y e. X \/ y e. { ( X F ( W ` X ) ) } ) )
135 133 134 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 ) ) } ) ) )
136 weso 
 |-  ( ( W ` X ) We X -> ( W ` X ) Or X )
137 20 136 syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( W ` X ) Or X )
138 solin 
 |-  ( ( ( W ` X ) Or X /\ ( x e. X /\ y e. X ) ) -> ( x ( W ` X ) y \/ x = y \/ y ( W ` X ) x ) )
139 137 138 sylan 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x ( W ` X ) y \/ x = y \/ y ( W ` X ) x ) )
140 ssun1 
 |-  ( W ` X ) C_ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
141 140 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 ) ) } ) ) )
142 141 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 ) )
143 idd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. X ) ) -> ( x = y -> x = y ) )
144 141 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 ) )
145 142 143 144 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 ) ) )
146 139 145 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 ) )
147 146 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 ) ) )
148 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 ) )
149 148 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 ) ) } ) )
150 brxp 
 |-  ( y ( X X. { ( X F ( W ` X ) ) } ) x <-> ( y e. X /\ x e. { ( X F ( W ` X ) ) } ) )
151 149 150 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 )
152 ssun2 
 |-  ( X X. { ( X F ( W ` X ) ) } ) C_ ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
153 152 ssbri 
 |-  ( y ( X X. { ( X F ( W ` X ) ) } ) x -> y ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) x )
154 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 ) )
155 151 153 154 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 ) )
156 155 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 ) ) )
157 brxp 
 |-  ( x ( X X. { ( X F ( W ` X ) ) } ) y <-> ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) )
158 157 bilanri 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ ( x e. X /\ y e. { ( X F ( W ` X ) ) } ) ) -> x ( X X. { ( X F ( W ` X ) ) } ) y )
159 152 ssbri 
 |-  ( x ( X X. { ( X F ( W ` X ) ) } ) y -> x ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
160 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 ) )
161 158 159 160 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 ) )
162 161 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 ) ) )
163 elsni 
 |-  ( x e. { ( X F ( W ` X ) ) } -> x = ( X F ( W ` X ) ) )
164 elsni 
 |-  ( y e. { ( X F ( W ` X ) ) } -> y = ( X F ( W ` X ) ) )
165 eqtr3 
 |-  ( ( x = ( X F ( W ` X ) ) /\ y = ( X F ( W ` X ) ) ) -> x = y )
166 163 164 165 syl2an 
 |-  ( ( x e. { ( X F ( W ` X ) ) } /\ y e. { ( X F ( W ` X ) ) } ) -> x = y )
167 166 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 ) )
168 167 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 ) ) )
169 147 156 162 168 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 ) ) )
170 135 169 biimtrid 
 |-  ( ( 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 ) ) )
171 170 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 ) )
172 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 ) ) )
173 132 171 172 sylanbrc 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) We ( X u. { ( X F ( W ` X ) ) } ) )
174 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 ) ) }
175 174 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 )
176 cnvimass 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) C_ dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) )
177 fvex 
 |-  ( W ` X ) e. _V
178 snex 
 |-  { ( X F ( W ` X ) ) } e. _V
179 xpexg 
 |-  ( ( X e. dom W /\ { ( X F ( W ` X ) ) } e. _V ) -> ( X X. { ( X F ( W ` X ) ) } ) e. _V )
180 8 178 179 sylancl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X X. { ( X F ( W ` X ) ) } ) e. _V )
181 unexg 
 |-  ( ( ( W ` X ) e. _V /\ ( X X. { ( X F ( W ` X ) ) } ) e. _V ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
182 177 180 181 sylancr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
183 182 dmexd 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> dom ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) e. _V )
184 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 )
185 176 183 184 sylancr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
186 185 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) e. _V )
187 id 
 |-  ( u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) -> u = ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) )
188 simpr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> y e. X )
189 simplr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> -. ( X F ( W ` X ) ) e. X )
190 nelne2 
 |-  ( ( y e. X /\ -. ( X F ( W ` X ) ) e. X ) -> y =/= ( X F ( W ` X ) ) )
191 188 189 190 syl2anc 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> y =/= ( X F ( W ` X ) ) )
192 86 164 syl 
 |-  ( z ( X X. { ( X F ( W ` X ) ) } ) y -> y = ( X F ( W ` X ) ) )
193 192 necon3ai 
 |-  ( y =/= ( X F ( W ` X ) ) -> -. z ( X X. { ( X F ( W ` X ) ) } ) y )
194 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 ) ) )
195 191 193 194 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 ) ) )
196 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 ) )
197 196 83 bitr4i 
 |-  ( ( z ( X X. { ( X F ( W ` X ) ) } ) y \/ z ( W ` X ) y ) <-> z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
198 195 197 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 ) )
199 vex 
 |-  z e. _V
200 199 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 ) )
201 200 elv 
 |-  ( z e. ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) <-> z ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) y )
202 199 eliniseg 
 |-  ( y e. _V -> ( z e. ( `' ( W ` X ) " { y } ) <-> z ( W ` X ) y ) )
203 202 elv 
 |-  ( z e. ( `' ( W ` X ) " { y } ) <-> z ( W ` X ) y )
204 198 201 203 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 } ) ) )
205 204 eqrdv 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( `' ( W ` X ) " { y } ) )
206 187 205 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 } ) )
207 206 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 } ) ) )
208 207 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 } ) ) ) )
209 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 } ) ) ) )
210 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 } ) ) )
211 incom 
 |-  ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) = ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } )
212 cnvimass 
 |-  ( `' ( W ` X ) " { y } ) C_ dom ( W ` X )
213 18 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( W ` X ) C_ ( X X. X ) )
214 dmss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
215 213 214 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> dom ( W ` X ) C_ dom ( X X. X ) )
216 dmxpid 
 |-  dom ( X X. X ) = X
217 215 216 sseqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> dom ( W ` X ) C_ X )
218 212 217 sstrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( `' ( W ` X ) " { y } ) C_ X )
219 218 189 ssneldd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> -. ( X F ( W ` X ) ) e. ( `' ( W ` X ) " { y } ) )
220 disjsn 
 |-  ( ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } ) = (/) <-> -. ( X F ( W ` X ) ) e. ( `' ( W ` X ) " { y } ) )
221 219 220 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( ( `' ( W ` X ) " { y } ) i^i { ( X F ( W ` X ) ) } ) = (/) )
222 211 221 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. X ) -> ( { ( X F ( W ` X ) ) } i^i ( `' ( W ` X ) " { y } ) ) = (/) )
223 222 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. (/) ) )
224 xp0 
 |-  ( ( X i^i ( `' ( W ` X ) " { y } ) ) X. (/) ) = (/)
225 223 224 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 } ) ) ) = (/) )
226 210 225 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 } ) ) ) = (/) )
227 226 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. (/) ) )
228 209 227 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. (/) ) )
229 un0 
 |-  ( ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) ) u. (/) ) = ( ( W ` X ) i^i ( ( `' ( W ` X ) " { y } ) X. ( `' ( W ` X ) " { y } ) ) )
230 228 229 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 } ) ) ) )
231 230 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 } ) ) ) )
232 208 231 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 } ) ) ) )
233 206 232 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 } ) ) ) ) )
234 233 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 ) )
235 186 234 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 ) )
236 175 235 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 )
237 164 adantl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> y = ( X F ( W ` X ) ) )
238 237 eqcomd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( X F ( W ` X ) ) = y )
239 185 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 )
240 simplr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> -. ( X F ( W ` X ) ) e. X )
241 237 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 ) ) )
242 18 adantr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( W ` X ) C_ ( X X. X ) )
243 rnss 
 |-  ( ( W ` X ) C_ ( X X. X ) -> ran ( W ` X ) C_ ran ( X X. X ) )
244 242 243 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ran ( W ` X ) C_ ran ( X X. X ) )
245 df-rn 
 |-  ran ( W ` X ) = dom `' ( W ` X )
246 rnxpid 
 |-  ran ( X X. X ) = X
247 244 245 246 3sstr3g 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> dom `' ( W ` X ) C_ X )
248 247 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 ) )
249 241 248 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 ) )
250 240 249 mtod 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> -. y e. dom `' ( W ` X ) )
251 ndmima 
 |-  ( -. y e. dom `' ( W ` X ) -> ( `' ( W ` X ) " { y } ) = (/) )
252 250 251 syl 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( W ` X ) " { y } ) = (/) )
253 237 sneqd 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> { y } = { ( X F ( W ` X ) ) } )
254 253 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 ) ) } ) )
255 df-ima 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) " { ( X F ( W ` X ) ) } ) = ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } )
256 cnvxp 
 |-  `' ( X X. { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
257 256 reseq1i 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ( ( { ( X F ( W ` X ) ) } X. X ) |` { ( X F ( W ` X ) ) } )
258 ssid 
 |-  { ( X F ( W ` X ) ) } C_ { ( X F ( W ` X ) ) }
259 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 ) )
260 258 259 ax-mp 
 |-  ( ( { ( X F ( W ` X ) ) } X. X ) |` { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
261 257 260 eqtri 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ( { ( X F ( W ` X ) ) } X. X )
262 261 rneqi 
 |-  ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = ran ( { ( X F ( W ` X ) ) } X. X )
263 46 snnz 
 |-  { ( X F ( W ` X ) ) } =/= (/)
264 rnxp 
 |-  ( { ( X F ( W ` X ) ) } =/= (/) -> ran ( { ( X F ( W ` X ) ) } X. X ) = X )
265 263 264 ax-mp 
 |-  ran ( { ( X F ( W ` X ) ) } X. X ) = X
266 262 265 eqtri 
 |-  ran ( `' ( X X. { ( X F ( W ` X ) ) } ) |` { ( X F ( W ` X ) ) } ) = X
267 255 266 eqtri 
 |-  ( `' ( X X. { ( X F ( W ` X ) ) } ) " { ( X F ( W ` X ) ) } ) = X
268 254 267 eqtrdi 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) = X )
269 252 268 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 ) )
270 cnvun 
 |-  `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) = ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) )
271 270 imaeq1i 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) ) " { y } )
272 imaundir 
 |-  ( ( `' ( W ` X ) u. `' ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) " { y } ) u. ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) )
273 271 272 eqtri 
 |-  ( `' ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) " { y } ) = ( ( `' ( W ` X ) " { y } ) u. ( `' ( X X. { ( X F ( W ` X ) ) } ) " { y } ) )
274 un0 
 |-  ( X u. (/) ) = X
275 uncom 
 |-  ( X u. (/) ) = ( (/) u. X )
276 274 275 eqtr3i 
 |-  X = ( (/) u. X )
277 269 273 276 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 )
278 187 277 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 )
279 278 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 ) )
280 279 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 ) ) )
281 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 ) ) )
282 dfss2 
 |-  ( ( W ` X ) C_ ( X X. X ) <-> ( ( W ` X ) i^i ( X X. X ) ) = ( W ` X ) )
283 242 282 sylib 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( ( W ` X ) i^i ( X X. X ) ) = ( W ` X ) )
284 incom 
 |-  ( { ( X F ( W ` X ) ) } i^i X ) = ( X i^i { ( X F ( W ` X ) ) } )
285 disjsn 
 |-  ( ( X i^i { ( X F ( W ` X ) ) } ) = (/) <-> -. ( X F ( W ` X ) ) e. X )
286 240 285 sylibr 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( X i^i { ( X F ( W ` X ) ) } ) = (/) )
287 284 286 eqtrid 
 |-  ( ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) /\ y e. { ( X F ( W ` X ) ) } ) -> ( { ( X F ( W ` X ) ) } i^i X ) = (/) )
288 287 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. (/) ) )
289 xpindi 
 |-  ( X X. ( { ( X F ( W ` X ) ) } i^i X ) ) = ( ( X X. { ( X F ( W ` X ) ) } ) i^i ( X X. X ) )
290 xp0 
 |-  ( X X. (/) ) = (/)
291 288 289 290 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 ) ) = (/) )
292 283 291 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. (/) ) )
293 281 292 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. (/) ) )
294 un0 
 |-  ( ( W ` X ) u. (/) ) = ( W ` X )
295 293 294 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 ) )
296 295 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 ) )
297 280 296 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 ) )
298 278 297 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 ) ) )
299 298 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 ) )
300 239 299 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 ) )
301 238 300 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 )
302 236 301 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 )
303 134 302 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 )
304 303 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 )
305 173 304 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 ) )
306 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 ) ) ) )
307 306 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 ) ) ) )
308 34 305 307 mpbir2and 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) W ( ( W ` X ) u. ( X X. { ( X F ( W ` X ) ) } ) ) )
309 1 relopabiv 
 |-  Rel W
310 309 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 )
311 elssuni 
 |-  ( ( X u. { ( X F ( W ` X ) ) } ) e. dom W -> ( X u. { ( X F ( W ` X ) ) } ) C_ U. dom W )
312 308 310 311 3syl 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) C_ U. dom W )
313 312 4 sseqtrrdi 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X u. { ( X F ( W ` X ) ) } ) C_ X )
314 5 313 sstrid 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> { ( X F ( W ` X ) ) } C_ X )
315 46 snss 
 |-  ( ( X F ( W ` X ) ) e. X <-> { ( X F ( W ` X ) ) } C_ X )
316 314 315 sylibr 
 |-  ( ( ph /\ -. ( X F ( W ` X ) ) e. X ) -> ( X F ( W ` X ) ) e. X )
317 316 pm2.18da 
 |-  ( ph -> ( X F ( W ` X ) ) e. X )