MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  fpwwe2 Unicode version

Theorem fpwwe2 8507
Description: Given any function  F from well-orderings of subsets of  A to  A, there is a unique well-ordered subset  <. X ,  ( W `  X )
>. which "agrees" with  F in the sense that each initial segment maps to its upper bound, and such that the entire set maps to an element of the set (so that it cannot be extended without losing the well-ordering). This theorem can be used to prove dfac8a 7900. Theorem 1.1 of [KanamoriPincus] p. 415. (Contributed by Mario Carneiro, 18-May-2015.)
Hypotheses
Ref Expression
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
Ref Expression
fpwwe2  |-  ( ph  ->  ( ( Y W R  /\  ( Y F R )  e.  Y )  <->  ( Y  =  X  /\  R  =  ( W `  X
) ) ) )
Distinct variable groups:    y, u, r, x, F    X, r, u, x, y    ph, r, u, x, y    A, r, x    R, r, u, x, y    Y, r, u, x, y    W, r, u, x, y
Allowed substitution hints:    A( y, u)

Proof of Theorem fpwwe2
Dummy variables  w  z are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fpwwe2.1 . . . . . . . . . . 11  |-  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 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  _V )
3 fpwwe2.3 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
4 fpwwe2.4 . . . . . . . . . . 11  |-  X  = 
U. dom  W
51, 2, 3, 4fpwwe2lem11 8504 . . . . . . . . . 10  |-  ( ph  ->  W : dom  W --> ~P ( X  X.  X
) )
6 ffun 5584 . . . . . . . . . 10  |-  ( W : dom  W --> ~P ( X  X.  X )  ->  Fun  W )
75, 6syl 16 . . . . . . . . 9  |-  ( ph  ->  Fun  W )
8 funbrfv2b 5762 . . . . . . . . 9  |-  ( Fun 
W  ->  ( Y W R  <->  ( Y  e. 
dom  W  /\  ( W `  Y )  =  R ) ) )
97, 8syl 16 . . . . . . . 8  |-  ( ph  ->  ( Y W R  <-> 
( Y  e.  dom  W  /\  ( W `  Y )  =  R ) ) )
109simprbda 607 . . . . . . 7  |-  ( (
ph  /\  Y W R )  ->  Y  e.  dom  W )
1110adantrr 698 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  Y  e.  dom  W )
12 elssuni 4035 . . . . . . 7  |-  ( Y  e.  dom  W  ->  Y  C_  U. dom  W
)
1312, 4syl6sseqr 3387 . . . . . 6  |-  ( Y  e.  dom  W  ->  Y  C_  X )
1411, 13syl 16 . . . . 5  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  Y  C_  X )
15 simpl 444 . . . . . . 7  |-  ( ( X  C_  Y  /\  ( W `  X )  =  ( R  i^i  ( Y  X.  X
) ) )  ->  X  C_  Y )
1615a1i 11 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( ( X  C_  Y  /\  ( W `  X )  =  ( R  i^i  ( Y  X.  X ) ) )  ->  X  C_  Y
) )
17 simplrr 738 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( Y F R )  e.  Y
)
182adantr 452 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  A  e.  _V )
1918adantr 452 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  A  e.  _V )
201, 2, 3, 4fpwwe2lem12 8505 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  X  e.  dom  W
)
21 funfvbrb 5834 . . . . . . . . . . . . . . . . . . . 20  |-  ( Fun 
W  ->  ( X  e.  dom  W  <->  X W
( W `  X
) ) )
227, 21syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  ( X  e.  dom  W  <-> 
X W ( W `
 X ) ) )
2320, 22mpbid 202 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  X W ( W `
 X ) )
241, 2fpwwe2lem2 8496 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( X W ( W `  X )  <-> 
( ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X ) )  /\  ( ( W `
 X )  We  X  /\  A. y  e.  X  [. ( `' ( W `  X
) " { y } )  /  u ]. ( u F ( ( W `  X
)  i^i  ( u  X.  u ) ) )  =  y ) ) ) )
2523, 24mpbid 202 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X ) )  /\  ( ( W `
 X )  We  X  /\  A. y  e.  X  [. ( `' ( W `  X
) " { y } )  /  u ]. ( u F ( ( W `  X
)  i^i  ( u  X.  u ) ) )  =  y ) ) )
2625ad2antrr 707 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( X 
C_  A  /\  ( W `  X )  C_  ( X  X.  X
) )  /\  (
( W `  X
)  We  X  /\  A. y  e.  X  [. ( `' ( W `  X ) " {
y } )  /  u ]. ( u F ( ( W `  X )  i^i  (
u  X.  u ) ) )  =  y ) ) )
2726simpld 446 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( X  C_  A  /\  ( W `  X )  C_  ( X  X.  X ) ) )
2827simpld 446 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  X  C_  A
)
2919, 28ssexd 4342 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  X  e.  _V )
30 difexg 4343 . . . . . . . . . . . . 13  |-  ( X  e.  _V  ->  ( X  \  Y )  e. 
_V )
3129, 30syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( X  \  Y )  e.  _V )
3226simprd 450 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( W `
 X )  We  X  /\  A. y  e.  X  [. ( `' ( W `  X
) " { y } )  /  u ]. ( u F ( ( W `  X
)  i^i  ( u  X.  u ) ) )  =  y ) )
3332simpld 446 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( W `  X )  We  X
)
34 wefr 4564 . . . . . . . . . . . . 13  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Fr  X )
3533, 34syl 16 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( W `  X )  Fr  X
)
36 difssd 3467 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( X  \  Y )  C_  X
)
37 fri 4536 . . . . . . . . . . . . 13  |-  ( ( ( ( X  \  Y )  e.  _V  /\  ( W `  X
)  Fr  X )  /\  ( ( X 
\  Y )  C_  X  /\  ( X  \  Y )  =/=  (/) ) )  ->  E. z  e.  ( X  \  Y ) A. w  e.  ( X  \  Y )  -.  w ( W `
 X ) z )
3837expr 599 . . . . . . . . . . . 12  |-  ( ( ( ( X  \  Y )  e.  _V  /\  ( W `  X
)  Fr  X )  /\  ( X  \  Y )  C_  X
)  ->  ( ( X  \  Y )  =/=  (/)  ->  E. z  e.  ( X  \  Y ) A. w  e.  ( X  \  Y )  -.  w ( W `
 X ) z ) )
3931, 35, 36, 38syl21anc 1183 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( X 
\  Y )  =/=  (/)  ->  E. z  e.  ( X  \  Y ) A. w  e.  ( X  \  Y )  -.  w ( W `
 X ) z ) )
40 ssdif0 3678 . . . . . . . . . . . . . . 15  |-  ( ( X  i^i  ( `' ( W `  X
) " { z } ) )  C_  Y 
<->  ( ( X  i^i  ( `' ( W `  X ) " {
z } ) ) 
\  Y )  =  (/) )
41 indif1 3577 . . . . . . . . . . . . . . . 16  |-  ( ( X  \  Y )  i^i  ( `' ( W `  X )
" { z } ) )  =  ( ( X  i^i  ( `' ( W `  X ) " {
z } ) ) 
\  Y )
4241eqeq1i 2442 . . . . . . . . . . . . . . 15  |-  ( ( ( X  \  Y
)  i^i  ( `' ( W `  X )
" { z } ) )  =  (/)  <->  (
( X  i^i  ( `' ( W `  X ) " {
z } ) ) 
\  Y )  =  (/) )
43 disj 3660 . . . . . . . . . . . . . . . 16  |-  ( ( ( X  \  Y
)  i^i  ( `' ( W `  X )
" { z } ) )  =  (/)  <->  A. w  e.  ( X  \  Y )  -.  w  e.  ( `' ( W `
 X ) " { z } ) )
44 vex 2951 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
45 vex 2951 . . . . . . . . . . . . . . . . . . . 20  |-  w  e. 
_V
4645eliniseg 5224 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  _V  ->  (
w  e.  ( `' ( W `  X
) " { z } )  <->  w ( W `  X )
z ) )
4744, 46ax-mp 8 . . . . . . . . . . . . . . . . . 18  |-  ( w  e.  ( `' ( W `  X )
" { z } )  <->  w ( W `
 X ) z )
4847notbii 288 . . . . . . . . . . . . . . . . 17  |-  ( -.  w  e.  ( `' ( W `  X
) " { z } )  <->  -.  w
( W `  X
) z )
4948ralbii 2721 . . . . . . . . . . . . . . . 16  |-  ( A. w  e.  ( X  \  Y )  -.  w  e.  ( `' ( W `
 X ) " { z } )  <->  A. w  e.  ( X  \  Y )  -.  w ( W `  X ) z )
5043, 49bitri 241 . . . . . . . . . . . . . . 15  |-  ( ( ( X  \  Y
)  i^i  ( `' ( W `  X )
" { z } ) )  =  (/)  <->  A. w  e.  ( X  \  Y )  -.  w
( W `  X
) z )
5140, 42, 503bitr2i 265 . . . . . . . . . . . . . 14  |-  ( ( X  i^i  ( `' ( W `  X
) " { z } ) )  C_  Y 
<-> 
A. w  e.  ( X  \  Y )  -.  w ( W `
 X ) z )
52 cnvimass 5215 . . . . . . . . . . . . . . . . 17  |-  ( `' ( W `  X
) " { z } )  C_  dom  ( W `  X )
5327simprd 450 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( W `  X )  C_  ( X  X.  X ) )
54 dmss 5060 . . . . . . . . . . . . . . . . . . 19  |-  ( ( W `  X ) 
C_  ( X  X.  X )  ->  dom  ( W `  X ) 
C_  dom  ( X  X.  X ) )
5553, 54syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  dom  ( W `  X )  C_  dom  ( X  X.  X
) )
56 dmxpid 5080 . . . . . . . . . . . . . . . . . 18  |-  dom  ( X  X.  X )  =  X
5755, 56syl6sseq 3386 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  dom  ( W `  X )  C_  X
)
5852, 57syl5ss 3351 . . . . . . . . . . . . . . . 16  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( `' ( W `  X )
" { z } )  C_  X )
59 dfss1 3537 . . . . . . . . . . . . . . . 16  |-  ( ( `' ( W `  X ) " {
z } )  C_  X 
<->  ( X  i^i  ( `' ( W `  X ) " {
z } ) )  =  ( `' ( W `  X )
" { z } ) )
6058, 59sylib 189 . . . . . . . . . . . . . . 15  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( X  i^i  ( `' ( W `  X ) " {
z } ) )  =  ( `' ( W `  X )
" { z } ) )
6160sseq1d 3367 . . . . . . . . . . . . . 14  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( X  i^i  ( `' ( W `  X )
" { z } ) )  C_  Y  <->  ( `' ( W `  X ) " {
z } )  C_  Y ) )
6251, 61syl5bbr 251 . . . . . . . . . . . . 13  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( A. w  e.  ( X  \  Y
)  -.  w ( W `  X ) z  <->  ( `' ( W `  X )
" { z } )  C_  Y )
)
6362rexbidv 2718 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( E. z  e.  ( X  \  Y
) A. w  e.  ( X  \  Y
)  -.  w ( W `  X ) z  <->  E. z  e.  ( X  \  Y ) ( `' ( W `
 X ) " { z } ) 
C_  Y ) )
64 eldifn 3462 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z  e.  ( X  \  Y )  ->  -.  z  e.  Y )
6564ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  -.  z  e.  Y
)
66 eleq1 2495 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( w  =  z  ->  (
w  e.  Y  <->  z  e.  Y ) )
6766notbid 286 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( w  =  z  ->  ( -.  w  e.  Y  <->  -.  z  e.  Y ) )
6865, 67syl5ibrcom 214 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( w  =  z  ->  -.  w  e.  Y ) )
6968con2d 109 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( w  e.  Y  ->  -.  w  =  z ) )
7069imp 419 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  -.  w  =  z )
7165adantr 452 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  -.  z  e.  Y )
72 simprr 734 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) )
7372ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) )
7473breqd 4215 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z R w  <->  z (
( W `  X
)  i^i  ( X  X.  Y ) ) w ) )
75 eldifi 3461 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( z  e.  ( X  \  Y )  ->  z  e.  X )
7675ad2antrl 709 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
z  e.  X )
7776adantr 452 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  z  e.  X )
78 simpr 448 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  w  e.  Y )
79 brxp 4900 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( X  X.  Y
) w  <->  ( z  e.  X  /\  w  e.  Y ) )
8077, 78, 79sylanbrc 646 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  z
( X  X.  Y
) w )
81 brin 4251 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( z ( ( W `  X )  i^i  ( X  X.  Y ) ) w  <->  ( z ( W `  X ) w  /\  z ( X  X.  Y ) w ) )
8281rbaib 874 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( X  X.  Y
) w  ->  (
z ( ( W `
 X )  i^i  ( X  X.  Y
) ) w  <->  z ( W `  X )
w ) )
8380, 82syl 16 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z ( ( W `
 X )  i^i  ( X  X.  Y
) ) w  <->  z ( W `  X )
w ) )
8474, 83bitrd 245 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z R w  <->  z ( W `  X )
w ) )
851, 2fpwwe2lem2 8496 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30  |-  ( ph  ->  ( Y W R  <-> 
( ( Y  C_  A  /\  R  C_  ( Y  X.  Y ) )  /\  ( R  We  Y  /\  A. y  e.  Y  [. ( `' R " { y } )  /  u ]. ( u F ( R  i^i  ( u  X.  u ) ) )  =  y ) ) ) )
8685biimpa 471 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29  |-  ( (
ph  /\  Y W R )  ->  (
( Y  C_  A  /\  R  C_  ( Y  X.  Y ) )  /\  ( R  We  Y  /\  A. y  e.  Y  [. ( `' R " { y } )  /  u ]. ( u F ( R  i^i  ( u  X.  u ) ) )  =  y ) ) )
8786adantrr 698 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( ( Y  C_  A  /\  R  C_  ( Y  X.  Y ) )  /\  ( R  We  Y  /\  A. y  e.  Y  [. ( `' R " { y } )  /  u ]. ( u F ( R  i^i  ( u  X.  u ) ) )  =  y ) ) )
8887simpld 446 . . . . . . . . . . . . . . . . . . . . . . . . . . 27  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( Y  C_  A  /\  R  C_  ( Y  X.  Y ) ) )
8988simprd 450 . . . . . . . . . . . . . . . . . . . . . . . . . 26  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  R  C_  ( Y  X.  Y ) )
9089ad3antrrr 711 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  R  C_  ( Y  X.  Y
) )
9190ssbrd 4245 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z R w  -> 
z ( Y  X.  Y ) w ) )
92 brxp 4900 . . . . . . . . . . . . . . . . . . . . . . . . 25  |-  ( z ( Y  X.  Y
) w  <->  ( z  e.  Y  /\  w  e.  Y ) )
9392simplbi 447 . . . . . . . . . . . . . . . . . . . . . . . 24  |-  ( z ( Y  X.  Y
) w  ->  z  e.  Y )
9491, 93syl6 31 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z R w  -> 
z  e.  Y ) )
9584, 94sylbird 227 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
z ( W `  X ) w  -> 
z  e.  Y ) )
9671, 95mtod 170 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  -.  z ( W `  X ) w )
9733ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  ( W `  X )  We  X )
98 weso 4565 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( W `  X )  We  X  ->  ( W `  X )  Or  X )
9997, 98syl 16 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  ( W `  X )  Or  X )
10014ad2antrr 707 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  Y  C_  X )
101100sselda 3340 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  w  e.  X )
102 sotric 4521 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( ( ( W `  X
)  Or  X  /\  ( w  e.  X  /\  z  e.  X
) )  ->  (
w ( W `  X ) z  <->  -.  (
w  =  z  \/  z ( W `  X ) w ) ) )
103 ioran 477 . . . . . . . . . . . . . . . . . . . . . . 23  |-  ( -.  ( w  =  z  \/  z ( W `
 X ) w )  <->  ( -.  w  =  z  /\  -.  z
( W `  X
) w ) )
104102, 103syl6bb 253 . . . . . . . . . . . . . . . . . . . . . 22  |-  ( ( ( W `  X
)  Or  X  /\  ( w  e.  X  /\  z  e.  X
) )  ->  (
w ( W `  X ) z  <->  ( -.  w  =  z  /\  -.  z ( W `  X ) w ) ) )
10599, 101, 77, 104syl12anc 1182 . . . . . . . . . . . . . . . . . . . . 21  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  (
w ( W `  X ) z  <->  ( -.  w  =  z  /\  -.  z ( W `  X ) w ) ) )
10670, 96, 105mpbir2and 889 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  w
( W `  X
) z )
107106, 47sylibr 204 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  w  e.  Y )  ->  w  e.  ( `' ( W `
 X ) " { z } ) )
108107ex 424 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( w  e.  Y  ->  w  e.  ( `' ( W `  X
) " { z } ) ) )
109108ssrdv 3346 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  Y  C_  ( `' ( W `  X )
" { z } ) )
110 simprr 734 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( `' ( W `
 X ) " { z } ) 
C_  Y )
111109, 110eqssd 3357 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  Y  =  ( `' ( W `  X )
" { z } ) )
112 in32 3545 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( W `  X
)  i^i  ( X  X.  Y ) )  i^i  ( Y  X.  Y
) )  =  ( ( ( W `  X )  i^i  ( Y  X.  Y ) )  i^i  ( X  X.  Y ) )
113 simplrr 738 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) )
114113ineq1d 3533 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( R  i^i  ( Y  X.  Y ) )  =  ( ( ( W `  X )  i^i  ( X  X.  Y ) )  i^i  ( Y  X.  Y
) ) )
11589ad2antrr 707 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  R  C_  ( Y  X.  Y ) )
116 df-ss 3326 . . . . . . . . . . . . . . . . . . . 20  |-  ( R 
C_  ( Y  X.  Y )  <->  ( R  i^i  ( Y  X.  Y
) )  =  R )
117115, 116sylib 189 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( R  i^i  ( Y  X.  Y ) )  =  R )
118114, 117eqtr3d 2469 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( ( ( W `
 X )  i^i  ( X  X.  Y
) )  i^i  ( Y  X.  Y ) )  =  R )
119 inss2 3554 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( W `  X )  i^i  ( Y  X.  Y ) )  C_  ( Y  X.  Y
)
120 xpss1 4975 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Y 
C_  X  ->  ( Y  X.  Y )  C_  ( X  X.  Y
) )
121100, 120syl 16 . . . . . . . . . . . . . . . . . . . 20  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( Y  X.  Y
)  C_  ( X  X.  Y ) )
122119, 121syl5ss 3351 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( ( W `  X )  i^i  ( Y  X.  Y ) ) 
C_  ( X  X.  Y ) )
123 df-ss 3326 . . . . . . . . . . . . . . . . . . 19  |-  ( ( ( W `  X
)  i^i  ( Y  X.  Y ) )  C_  ( X  X.  Y
)  <->  ( ( ( W `  X )  i^i  ( Y  X.  Y ) )  i^i  ( X  X.  Y
) )  =  ( ( W `  X
)  i^i  ( Y  X.  Y ) ) )
124122, 123sylib 189 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( ( ( W `
 X )  i^i  ( Y  X.  Y
) )  i^i  ( X  X.  Y ) )  =  ( ( W `
 X )  i^i  ( Y  X.  Y
) ) )
125112, 118, 1243eqtr3a 2491 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  R  =  ( ( W `  X )  i^i  ( Y  X.  Y
) ) )
126111, 111xpeq12d 4894 . . . . . . . . . . . . . . . . . 18  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( Y  X.  Y
)  =  ( ( `' ( W `  X ) " {
z } )  X.  ( `' ( W `
 X ) " { z } ) ) )
127126ineq2d 3534 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( ( W `  X )  i^i  ( Y  X.  Y ) )  =  ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { z } )  X.  ( `' ( W `  X
) " { z } ) ) ) )
128125, 127eqtrd 2467 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  R  =  ( ( W `  X )  i^i  ( ( `' ( W `  X )
" { z } )  X.  ( `' ( W `  X
) " { z } ) ) ) )
129111, 128oveq12d 6090 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( Y F R )  =  ( ( `' ( W `  X ) " {
z } ) F ( ( W `  X )  i^i  (
( `' ( W `
 X ) " { z } )  X.  ( `' ( W `  X )
" { z } ) ) ) ) )
13019adantr 452 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  A  e.  _V )
13123adantr 452 . . . . . . . . . . . . . . . . . 18  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  X W ( W `  X ) )
132131ad2antrr 707 . . . . . . . . . . . . . . . . 17  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  X W ( W `  X ) )
1331, 130, 132fpwwe2lem3 8497 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y
) )  /\  ( Y  C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) )  /\  ( z  e.  ( X  \  Y
)  /\  ( `' ( W `  X )
" { z } )  C_  Y )
)  /\  z  e.  X )  ->  (
( `' ( W `
 X ) " { z } ) F ( ( W `
 X )  i^i  ( ( `' ( W `  X )
" { z } )  X.  ( `' ( W `  X
) " { z } ) ) ) )  =  z )
13476, 133mpdan 650 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( ( `' ( W `  X )
" { z } ) F ( ( W `  X )  i^i  ( ( `' ( W `  X
) " { z } )  X.  ( `' ( W `  X ) " {
z } ) ) ) )  =  z )
135129, 134eqtrd 2467 . . . . . . . . . . . . . 14  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  -> 
( Y F R )  =  z )
136135, 65eqneltrd 2528 . . . . . . . . . . . . 13  |-  ( ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) ) )  /\  ( z  e.  ( X  \  Y )  /\  ( `' ( W `  X ) " {
z } )  C_  Y ) )  ->  -.  ( Y F R )  e.  Y )
137136rexlimdvaa 2823 . . . . . . . . . . . 12  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( E. z  e.  ( X  \  Y
) ( `' ( W `  X )
" { z } )  C_  Y  ->  -.  ( Y F R )  e.  Y ) )
13863, 137sylbid 207 . . . . . . . . . . 11  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( E. z  e.  ( X  \  Y
) A. w  e.  ( X  \  Y
)  -.  w ( W `  X ) z  ->  -.  ( Y F R )  e.  Y ) )
13939, 138syld 42 . . . . . . . . . 10  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( X 
\  Y )  =/=  (/)  ->  -.  ( Y F R )  e.  Y
) )
140139necon4ad 2659 . . . . . . . . 9  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( ( Y F R )  e.  Y  ->  ( X  \  Y )  =  (/) ) )
14117, 140mpd 15 . . . . . . . 8  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  ( X  \  Y )  =  (/) )
142 ssdif0 3678 . . . . . . . 8  |-  ( X 
C_  Y  <->  ( X  \  Y )  =  (/) )
143141, 142sylibr 204 . . . . . . 7  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( Y  C_  X  /\  R  =  ( ( W `  X )  i^i  ( X  X.  Y
) ) ) )  ->  X  C_  Y
)
144143ex 424 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( ( Y  C_  X  /\  R  =  ( ( W `  X
)  i^i  ( X  X.  Y ) ) )  ->  X  C_  Y
) )
1453adantlr 696 . . . . . . 7  |-  ( ( ( ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  /\  ( x  C_  A  /\  r  C_  ( x  X.  x )  /\  r  We  x ) )  -> 
( x F r )  e.  A )
146 simprl 733 . . . . . . 7  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  Y W R )
1471, 18, 145, 131, 146fpwwe2lem10 8503 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( ( X  C_  Y  /\  ( W `  X )  =  ( R  i^i  ( Y  X.  X ) ) )  \/  ( Y 
C_  X  /\  R  =  ( ( W `
 X )  i^i  ( X  X.  Y
) ) ) ) )
14816, 144, 147mpjaod 371 . . . . 5  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  X  C_  Y )
14914, 148eqssd 3357 . . . 4  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  Y  =  X )
1507adantr 452 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  Fun  W )
151149, 146eqbrtrrd 4226 . . . . . 6  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  X W R )
152 funbrfv 5756 . . . . . 6  |-  ( Fun 
W  ->  ( X W R  ->  ( W `
 X )  =  R ) )
153150, 151, 152sylc 58 . . . . 5  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( W `  X
)  =  R )
154153eqcomd 2440 . . . 4  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  ->  R  =  ( W `  X ) )
155149, 154jca 519 . . 3  |-  ( (
ph  /\  ( Y W R  /\  ( Y F R )  e.  Y ) )  -> 
( Y  =  X  /\  R  =  ( W `  X ) ) )
156155ex 424 . 2  |-  ( ph  ->  ( ( Y W R  /\  ( Y F R )  e.  Y )  ->  ( Y  =  X  /\  R  =  ( W `  X ) ) ) )
1571, 2, 3, 4fpwwe2lem13 8506 . . . 4  |-  ( ph  ->  ( X F ( W `  X ) )  e.  X )
15823, 157jca 519 . . 3  |-  ( ph  ->  ( X W ( W `  X )  /\  ( X F ( W `  X
) )  e.  X
) )
159 breq12 4209 . . . 4  |-  ( ( Y  =  X  /\  R  =  ( W `  X ) )  -> 
( Y W R  <-> 
X W ( W `
 X ) ) )
160 oveq12 6081 . . . . 5  |-  ( ( Y  =  X  /\  R  =  ( W `  X ) )  -> 
( Y F R )  =  ( X F ( W `  X ) ) )
161 simpl 444 . . . . 5  |-  ( ( Y  =  X  /\  R  =  ( W `  X ) )  ->  Y  =  X )
162160, 161eleq12d 2503 . . . 4  |-  ( ( Y  =  X  /\  R  =  ( W `  X ) )  -> 
( ( Y F R )  e.  Y  <->  ( X F ( W `
 X ) )  e.  X ) )
163159, 162anbi12d 692 . . 3  |-  ( ( Y  =  X  /\  R  =  ( W `  X ) )  -> 
( ( Y W R  /\  ( Y F R )  e.  Y )  <->  ( X W ( W `  X )  /\  ( X F ( W `  X ) )  e.  X ) ) )
164158, 163syl5ibrcom 214 . 2  |-  ( ph  ->  ( ( Y  =  X  /\  R  =  ( W `  X
) )  ->  ( Y W R  /\  ( Y F R )  e.  Y ) ) )
165156, 164impbid 184 1  |-  ( ph  ->  ( ( Y W R  /\  ( Y F R )  e.  Y )  <->  ( Y  =  X  /\  R  =  ( W `  X
) ) ) )
Colors of variables: wff set class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 177    \/ wo 358    /\ wa 359    /\ w3a 936    = wceq 1652    e. wcel 1725    =/= wne 2598   A.wral 2697   E.wrex 2698   _Vcvv 2948   [.wsbc 3153    \ cdif 3309    i^i cin 3311    C_ wss 3312   (/)c0 3620   ~Pcpw 3791   {csn 3806   U.cuni 4007   class class class wbr 4204   {copab 4257    Or wor 4494    Fr wfr 4530    We wwe 4532    X. cxp 4867   `'ccnv 4868   dom cdm 4869   "cima 4872   Fun wfun 5439   -->wf 5441   ` cfv 5445  (class class class)co 6072
This theorem is referenced by:  fpwwe  8510  canthwelem  8514  pwfseqlem4  8526
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-13 1727  ax-14 1729  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2416  ax-rep 4312  ax-sep 4322  ax-nul 4330  ax-pow 4369  ax-pr 4395  ax-un 4692
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-eu 2284  df-mo 2285  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-ral 2702  df-rex 2703  df-reu 2704  df-rmo 2705  df-rab 2706  df-v 2950  df-sbc 3154  df-csb 3244  df-dif 3315  df-un 3317  df-in 3319  df-ss 3326  df-pss 3328  df-nul 3621  df-if 3732  df-pw 3793  df-sn 3812  df-pr 3813  df-tp 3814  df-op 3815  df-uni 4008  df-iun 4087  df-br 4205  df-opab 4259  df-mpt 4260  df-tr 4295  df-eprel 4486  df-id 4490  df-po 4495  df-so 4496  df-fr 4533  df-se 4534  df-we 4535  df-ord 4576  df-on 4577  df-lim 4578  df-suc 4579  df-xp 4875  df-rel 4876  df-cnv 4877  df-co 4878  df-dm 4879  df-rn 4880  df-res 4881  df-ima 4882  df-iota 5409  df-fun 5447  df-fn 5448  df-f 5449  df-f1 5450  df-fo 5451  df-f1o 5452  df-fv 5453  df-isom 5454  df-ov 6075  df-riota 6540  df-recs 6624  df-oi 7468
  Copyright terms: Public domain W3C validator