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

Theorem fpwwe2lem9 8276
Description: Lemma for fpwwe2 8281. Given two well-orders  <. X ,  R >. and  <. Y ,  S >. of parts of  A, one is an initial segment of the other. (The  O  C_  P hypothesis is in order to break the symmetry of  X and  Y.) (Contributed by Mario Carneiro, 15-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 )
fpwwe2lem9.x  |-  ( ph  ->  X W R )
fpwwe2lem9.y  |-  ( ph  ->  Y W S )
fpwwe2lem9.m  |-  M  = OrdIso
( R ,  X
)
fpwwe2lem9.n  |-  N  = OrdIso
( S ,  Y
)
fpwwe2lem9.s  |-  ( ph  ->  dom  M  C_  dom  N )
Assertion
Ref Expression
fpwwe2lem9  |-  ( ph  ->  ( X  C_  Y  /\  R  =  ( S  i^i  ( Y  X.  X ) ) ) )
Distinct variable groups:    y, u, r, x, F    X, r, u, x, y    M, r, u, x, y    N, r, u, x, y    ph, r, u, x, y    A, r, x    R, r, u, x, y    Y, r, u, x, y    S, r, u, x, y    W, r, u, x, y
Allowed substitution hints:    A( y, u)

Proof of Theorem fpwwe2lem9
StepHypRef Expression
1 fpwwe2lem9.x . . . . . . . . 9  |-  ( ph  ->  X W R )
2 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 ) ) }
32relopabi 4827 . . . . . . . . . 10  |-  Rel  W
43brrelexi 4745 . . . . . . . . 9  |-  ( X W R  ->  X  e.  _V )
51, 4syl 15 . . . . . . . 8  |-  ( ph  ->  X  e.  _V )
6 fpwwe2.2 . . . . . . . . . . . 12  |-  ( ph  ->  A  e.  _V )
72, 6fpwwe2lem2 8270 . . . . . . . . . . 11  |-  ( ph  ->  ( X W 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 ) ) ) )
81, 7mpbid 201 . . . . . . . . . 10  |-  ( ph  ->  ( ( 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 ) ) )
98simprd 449 . . . . . . . . 9  |-  ( ph  ->  ( R  We  X  /\  A. y  e.  X  [. ( `' R " { y } )  /  u ]. (
u F ( R  i^i  ( u  X.  u ) ) )  =  y ) )
109simpld 445 . . . . . . . 8  |-  ( ph  ->  R  We  X )
11 fpwwe2lem9.m . . . . . . . . 9  |-  M  = OrdIso
( R ,  X
)
1211oiiso 7268 . . . . . . . 8  |-  ( ( X  e.  _V  /\  R  We  X )  ->  M  Isom  _E  ,  R  ( dom  M ,  X
) )
135, 10, 12syl2anc 642 . . . . . . 7  |-  ( ph  ->  M  Isom  _E  ,  R  ( dom  M ,  X
) )
14 isof1o 5838 . . . . . . 7  |-  ( M 
Isom  _E  ,  R  ( dom  M ,  X
)  ->  M : dom  M -1-1-onto-> X )
1513, 14syl 15 . . . . . 6  |-  ( ph  ->  M : dom  M -1-1-onto-> X
)
16 f1ofo 5495 . . . . . 6  |-  ( M : dom  M -1-1-onto-> X  ->  M : dom  M -onto-> X
)
17 forn 5470 . . . . . 6  |-  ( M : dom  M -onto-> X  ->  ran  M  =  X )
1815, 16, 173syl 18 . . . . 5  |-  ( ph  ->  ran  M  =  X )
19 fpwwe2.3 . . . . . . 7  |-  ( (
ph  /\  ( x  C_  A  /\  r  C_  ( x  X.  x
)  /\  r  We  x ) )  -> 
( x F r )  e.  A )
20 fpwwe2lem9.y . . . . . . 7  |-  ( ph  ->  Y W S )
21 fpwwe2lem9.n . . . . . . 7  |-  N  = OrdIso
( S ,  Y
)
22 fpwwe2lem9.s . . . . . . 7  |-  ( ph  ->  dom  M  C_  dom  N )
232, 6, 19, 1, 20, 11, 21, 22fpwwe2lem8 8275 . . . . . 6  |-  ( ph  ->  M  =  ( N  |`  dom  M ) )
2423rneqd 4922 . . . . 5  |-  ( ph  ->  ran  M  =  ran  ( N  |`  dom  M
) )
2518, 24eqtr3d 2330 . . . 4  |-  ( ph  ->  X  =  ran  ( N  |`  dom  M ) )
26 df-ima 4718 . . . 4  |-  ( N
" dom  M )  =  ran  ( N  |`  dom  M )
2725, 26syl6eqr 2346 . . 3  |-  ( ph  ->  X  =  ( N
" dom  M )
)
28 imassrn 5041 . . . 4  |-  ( N
" dom  M )  C_ 
ran  N
293brrelexi 4745 . . . . . . . 8  |-  ( Y W S  ->  Y  e.  _V )
3020, 29syl 15 . . . . . . 7  |-  ( ph  ->  Y  e.  _V )
312, 6fpwwe2lem2 8270 . . . . . . . . . 10  |-  ( ph  ->  ( Y W S  <-> 
( ( Y  C_  A  /\  S  C_  ( Y  X.  Y ) )  /\  ( S  We  Y  /\  A. y  e.  Y  [. ( `' S " { y } )  /  u ]. ( u F ( S  i^i  ( u  X.  u ) ) )  =  y ) ) ) )
3220, 31mpbid 201 . . . . . . . . 9  |-  ( ph  ->  ( ( Y  C_  A  /\  S  C_  ( Y  X.  Y ) )  /\  ( S  We  Y  /\  A. y  e.  Y  [. ( `' S " { y } )  /  u ]. ( u F ( S  i^i  ( u  X.  u ) ) )  =  y ) ) )
3332simprd 449 . . . . . . . 8  |-  ( ph  ->  ( S  We  Y  /\  A. y  e.  Y  [. ( `' S " { y } )  /  u ]. (
u F ( S  i^i  ( u  X.  u ) ) )  =  y ) )
3433simpld 445 . . . . . . 7  |-  ( ph  ->  S  We  Y )
3521oiiso 7268 . . . . . . 7  |-  ( ( Y  e.  _V  /\  S  We  Y )  ->  N  Isom  _E  ,  S  ( dom  N ,  Y
) )
3630, 34, 35syl2anc 642 . . . . . 6  |-  ( ph  ->  N  Isom  _E  ,  S  ( dom  N ,  Y
) )
37 isof1o 5838 . . . . . 6  |-  ( N 
Isom  _E  ,  S  ( dom  N ,  Y
)  ->  N : dom  N -1-1-onto-> Y )
3836, 37syl 15 . . . . 5  |-  ( ph  ->  N : dom  N -1-1-onto-> Y
)
39 f1ofo 5495 . . . . 5  |-  ( N : dom  N -1-1-onto-> Y  ->  N : dom  N -onto-> Y
)
40 forn 5470 . . . . 5  |-  ( N : dom  N -onto-> Y  ->  ran  N  =  Y )
4138, 39, 403syl 18 . . . 4  |-  ( ph  ->  ran  N  =  Y )
4228, 41syl5sseq 3239 . . 3  |-  ( ph  ->  ( N " dom  M )  C_  Y )
4327, 42eqsstrd 3225 . 2  |-  ( ph  ->  X  C_  Y )
448simpld 445 . . . . . 6  |-  ( ph  ->  ( X  C_  A  /\  R  C_  ( X  X.  X ) ) )
4544simprd 449 . . . . 5  |-  ( ph  ->  R  C_  ( X  X.  X ) )
46 relxp 4810 . . . . 5  |-  Rel  ( X  X.  X )
47 relss 4791 . . . . 5  |-  ( R 
C_  ( X  X.  X )  ->  ( Rel  ( X  X.  X
)  ->  Rel  R ) )
4845, 46, 47ee10 1366 . . . 4  |-  ( ph  ->  Rel  R )
49 inss2 3403 . . . . 5  |-  ( S  i^i  ( Y  X.  X ) )  C_  ( Y  X.  X
)
50 relxp 4810 . . . . 5  |-  Rel  ( Y  X.  X )
51 relss 4791 . . . . 5  |-  ( ( S  i^i  ( Y  X.  X ) ) 
C_  ( Y  X.  X )  ->  ( Rel  ( Y  X.  X
)  ->  Rel  ( S  i^i  ( Y  X.  X ) ) ) )
5249, 50, 51mp2 17 . . . 4  |-  Rel  ( S  i^i  ( Y  X.  X ) )
5348, 52jctir 524 . . 3  |-  ( ph  ->  ( Rel  R  /\  Rel  ( S  i^i  ( Y  X.  X ) ) ) )
5445ssbrd 4080 . . . . . . 7  |-  ( ph  ->  ( x R y  ->  x ( X  X.  X ) y ) )
55 brxp 4736 . . . . . . 7  |-  ( x ( X  X.  X
) y  <->  ( x  e.  X  /\  y  e.  X ) )
5654, 55syl6ib 217 . . . . . 6  |-  ( ph  ->  ( x R y  ->  ( x  e.  X  /\  y  e.  X ) ) )
57 brinxp2 4767 . . . . . . . 8  |-  ( x ( S  i^i  ( Y  X.  X ) ) y  <->  ( x  e.  Y  /\  y  e.  X  /\  x S y ) )
58 df-3an 936 . . . . . . . 8  |-  ( ( x  e.  Y  /\  y  e.  X  /\  x S y )  <->  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )
5957, 58bitri 240 . . . . . . 7  |-  ( x ( S  i^i  ( Y  X.  X ) ) y  <->  ( ( x  e.  Y  /\  y  e.  X )  /\  x S y ) )
60 simprll 738 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  x  e.  Y )
61 simprr 733 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  x S
y )
62 isocnv 5843 . . . . . . . . . . . . . . . . 17  |-  ( N 
Isom  _E  ,  S  ( dom  N ,  Y
)  ->  `' N  Isom  S ,  _E  ( Y ,  dom  N ) )
6336, 62syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  `' N  Isom  S ,  _E  ( Y ,  dom  N ) )
6463adantr 451 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' N  Isom  S ,  _E  ( Y ,  dom  N ) )
6543adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  X  C_  Y
)
66 simprlr 739 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  y  e.  X )
6765, 66sseldd 3194 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  y  e.  Y )
68 isorel 5839 . . . . . . . . . . . . . . 15  |-  ( ( `' N  Isom  S ,  _E  ( Y ,  dom  N )  /\  ( x  e.  Y  /\  y  e.  Y ) )  -> 
( x S y  <-> 
( `' N `  x )  _E  ( `' N `  y ) ) )
6964, 60, 67, 68syl12anc 1180 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( x S y  <->  ( `' N `  x )  _E  ( `' N `  y ) ) )
7061, 69mpbid 201 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' N `  x )  _E  ( `' N `  y ) )
71 fvex 5555 . . . . . . . . . . . . . 14  |-  ( `' N `  y )  e.  _V
7271epelc 4323 . . . . . . . . . . . . 13  |-  ( ( `' N `  x )  _E  ( `' N `  y )  <->  ( `' N `  x )  e.  ( `' N `  y ) )
7370, 72sylib 188 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' N `  x )  e.  ( `' N `  y ) )
7423adantr 451 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  M  =  ( N  |`  dom  M
) )
7574cnveqd 4873 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' M  =  `' ( N  |`  dom  M ) )
76 isof1o 5838 . . . . . . . . . . . . . . . . . 18  |-  ( `' N  Isom  S ,  _E  ( Y ,  dom  N )  ->  `' N : Y -1-1-onto-> dom  N )
77 f1ofn 5489 . . . . . . . . . . . . . . . . . 18  |-  ( `' N : Y -1-1-onto-> dom  N  ->  `' N  Fn  Y
)
7864, 76, 773syl 18 . . . . . . . . . . . . . . . . 17  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' N  Fn  Y )
79 fnfun 5357 . . . . . . . . . . . . . . . . 17  |-  ( `' N  Fn  Y  ->  Fun  `' N )
80 funcnvres 5337 . . . . . . . . . . . . . . . . 17  |-  ( Fun  `' N  ->  `' ( N  |`  dom  M )  =  ( `' N  |`  ( N " dom  M ) ) )
8178, 79, 803syl 18 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' ( N  |`  dom  M )  =  ( `' N  |`  ( N " dom  M ) ) )
8275, 81eqtrd 2328 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' M  =  ( `' N  |`  ( N " dom  M ) ) )
8382fveq1d 5543 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' M `  y )  =  ( ( `' N  |`  ( N " dom  M ) ) `
 y ) )
8427adantr 451 . . . . . . . . . . . . . . . 16  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  X  =  ( N " dom  M
) )
8566, 84eleqtrd 2372 . . . . . . . . . . . . . . 15  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  y  e.  ( N " dom  M
) )
86 fvres 5558 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( N " dom  M )  ->  (
( `' N  |`  ( N " dom  M
) ) `  y
)  =  ( `' N `  y ) )
8785, 86syl 15 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( ( `' N  |`  ( N
" dom  M )
) `  y )  =  ( `' N `  y ) )
8883, 87eqtrd 2328 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' M `  y )  =  ( `' N `  y ) )
89 isocnv 5843 . . . . . . . . . . . . . . . . 17  |-  ( M 
Isom  _E  ,  R  ( dom  M ,  X
)  ->  `' M  Isom  R ,  _E  ( X ,  dom  M ) )
9013, 89syl 15 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  `' M  Isom  R ,  _E  ( X ,  dom  M ) )
91 isof1o 5838 . . . . . . . . . . . . . . . 16  |-  ( `' M  Isom  R ,  _E  ( X ,  dom  M )  ->  `' M : X -1-1-onto-> dom  M )
92 f1of 5488 . . . . . . . . . . . . . . . 16  |-  ( `' M : X -1-1-onto-> dom  M  ->  `' M : X --> dom  M
)
9390, 91, 923syl 18 . . . . . . . . . . . . . . 15  |-  ( ph  ->  `' M : X --> dom  M
)
9493adantr 451 . . . . . . . . . . . . . 14  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  `' M : X --> dom  M )
95 ffvelrn 5679 . . . . . . . . . . . . . 14  |-  ( ( `' M : X --> dom  M  /\  y  e.  X
)  ->  ( `' M `  y )  e.  dom  M )
9694, 66, 95syl2anc 642 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' M `  y )  e.  dom  M )
9788, 96eqeltrrd 2371 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' N `  y )  e.  dom  M )
9811oicl 7260 . . . . . . . . . . . . 13  |-  Ord  dom  M
99 ordtr1 4451 . . . . . . . . . . . . 13  |-  ( Ord 
dom  M  ->  ( ( ( `' N `  x )  e.  ( `' N `  y )  /\  ( `' N `  y )  e.  dom  M )  ->  ( `' N `  x )  e.  dom  M ) )
10098, 99ax-mp 8 . . . . . . . . . . . 12  |-  ( ( ( `' N `  x )  e.  ( `' N `  y )  /\  ( `' N `  y )  e.  dom  M )  ->  ( `' N `  x )  e.  dom  M )
10173, 97, 100syl2anc 642 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( `' N `  x )  e.  dom  M )
102 elpreima 5661 . . . . . . . . . . . 12  |-  ( `' N  Fn  Y  -> 
( x  e.  ( `' `' N " dom  M
)  <->  ( x  e.  Y  /\  ( `' N `  x )  e.  dom  M ) ) )
10378, 102syl 15 . . . . . . . . . . 11  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( x  e.  ( `' `' N " dom  M )  <->  ( x  e.  Y  /\  ( `' N `  x )  e.  dom  M ) ) )
10460, 101, 103mpbir2and 888 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  x  e.  ( `' `' N " dom  M
) )
105 imacnvcnv 5153 . . . . . . . . . . 11  |-  ( `' `' N " dom  M
)  =  ( N
" dom  M )
10684, 105syl6eqr 2346 . . . . . . . . . 10  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  X  =  ( `' `' N " dom  M
) )
107104, 106eleqtrrd 2373 . . . . . . . . 9  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  x  e.  X )
108107, 66jca 518 . . . . . . . 8  |-  ( (
ph  /\  ( (
x  e.  Y  /\  y  e.  X )  /\  x S y ) )  ->  ( x  e.  X  /\  y  e.  X ) )
109108ex 423 . . . . . . 7  |-  ( ph  ->  ( ( ( x  e.  Y  /\  y  e.  X )  /\  x S y )  -> 
( x  e.  X  /\  y  e.  X
) ) )
11059, 109syl5bi 208 . . . . . 6  |-  ( ph  ->  ( x ( S  i^i  ( Y  X.  X ) ) y  ->  ( x  e.  X  /\  y  e.  X ) ) )
11123adantr 451 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  M  =  ( N  |` 
dom  M ) )
112111cnveqd 4873 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  `' M  =  `' ( N  |`  dom  M
) )
113112fveq1d 5543 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( `' M `  x )  =  ( `' ( N  |`  dom  M ) `  x
) )
114112fveq1d 5543 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( `' M `  y )  =  ( `' ( N  |`  dom  M ) `  y
) )
115113, 114breq12d 4052 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( ( `' M `  x )  _E  ( `' M `  y )  <-> 
( `' ( N  |`  dom  M ) `  x )  _E  ( `' ( N  |`  dom  M ) `  y
) ) )
116 isorel 5839 . . . . . . . . . 10  |-  ( ( `' M  Isom  R ,  _E  ( X ,  dom  M )  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x R y  <-> 
( `' M `  x )  _E  ( `' M `  y ) ) )
11790, 116sylan 457 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x R y  <-> 
( `' M `  x )  _E  ( `' M `  y ) ) )
118 eqidd 2297 . . . . . . . . . . . . 13  |-  ( ph  ->  ( N " dom  M )  =  ( N
" dom  M )
)
119 isores3 5848 . . . . . . . . . . . . 13  |-  ( ( N  Isom  _E  ,  S  ( dom  N ,  Y
)  /\  dom  M  C_  dom  N  /\  ( N
" dom  M )  =  ( N " dom  M ) )  -> 
( N  |`  dom  M
)  Isom  _E  ,  S  ( dom  M ,  ( N " dom  M
) ) )
12036, 22, 118, 119syl3anc 1182 . . . . . . . . . . . 12  |-  ( ph  ->  ( N  |`  dom  M
)  Isom  _E  ,  S  ( dom  M ,  ( N " dom  M
) ) )
121 isocnv 5843 . . . . . . . . . . . 12  |-  ( ( N  |`  dom  M ) 
Isom  _E  ,  S  ( dom  M ,  ( N " dom  M
) )  ->  `' ( N  |`  dom  M
)  Isom  S ,  _E  ( ( N " dom  M ) ,  dom  M ) )
122120, 121syl 15 . . . . . . . . . . 11  |-  ( ph  ->  `' ( N  |`  dom  M )  Isom  S ,  _E  ( ( N " dom  M ) ,  dom  M ) )
123122adantr 451 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  `' ( N  |`  dom  M )  Isom  S ,  _E  ( ( N " dom  M ) ,  dom  M ) )
124 simprl 732 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  x  e.  X )
12527adantr 451 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  X  =  ( N " dom  M ) )
126124, 125eleqtrd 2372 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  x  e.  ( N " dom  M ) )
127 simprr 733 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
y  e.  X )
128127, 125eleqtrd 2372 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
y  e.  ( N
" dom  M )
)
129 isorel 5839 . . . . . . . . . 10  |-  ( ( `' ( N  |`  dom  M )  Isom  S ,  _E  ( ( N " dom  M ) ,  dom  M )  /\  ( x  e.  ( N " dom  M )  /\  y  e.  ( N " dom  M ) ) )  -> 
( x S y  <-> 
( `' ( N  |`  dom  M ) `  x )  _E  ( `' ( N  |`  dom  M ) `  y
) ) )
130123, 126, 128, 129syl12anc 1180 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x S y  <-> 
( `' ( N  |`  dom  M ) `  x )  _E  ( `' ( N  |`  dom  M ) `  y
) ) )
131115, 117, 1303bitr4d 276 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x R y  <-> 
x S y ) )
13243sselda 3193 . . . . . . . . . . . 12  |-  ( (
ph  /\  x  e.  X )  ->  x  e.  Y )
133132adantrr 697 . . . . . . . . . . 11  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  ->  x  e.  Y )
134133, 127jca 518 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x  e.  Y  /\  y  e.  X
) )
135134biantrurd 494 . . . . . . . . 9  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x S y  <-> 
( ( x  e.  Y  /\  y  e.  X )  /\  x S y ) ) )
136135, 59syl6bbr 254 . . . . . . . 8  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x S y  <-> 
x ( S  i^i  ( Y  X.  X
) ) y ) )
137131, 136bitrd 244 . . . . . . 7  |-  ( (
ph  /\  ( x  e.  X  /\  y  e.  X ) )  -> 
( x R y  <-> 
x ( S  i^i  ( Y  X.  X
) ) y ) )
138137ex 423 . . . . . 6  |-  ( ph  ->  ( ( x  e.  X  /\  y  e.  X )  ->  (
x R y  <->  x ( S  i^i  ( Y  X.  X ) ) y ) ) )
13956, 110, 138pm5.21ndd 343 . . . . 5  |-  ( ph  ->  ( x R y  <-> 
x ( S  i^i  ( Y  X.  X
) ) y ) )
140 df-br 4040 . . . . 5  |-  ( x R y  <->  <. x ,  y >.  e.  R
)
141 df-br 4040 . . . . 5  |-  ( x ( S  i^i  ( Y  X.  X ) ) y  <->  <. x ,  y
>.  e.  ( S  i^i  ( Y  X.  X
) ) )
142139, 140, 1413bitr3g 278 . . . 4  |-  ( ph  ->  ( <. x ,  y
>.  e.  R  <->  <. x ,  y >.  e.  ( S  i^i  ( Y  X.  X ) ) ) )
143142eqrelrdv2 4802 . . 3  |-  ( ( ( Rel  R  /\  Rel  ( S  i^i  ( Y  X.  X ) ) )  /\  ph )  ->  R  =  ( S  i^i  ( Y  X.  X ) ) )
14453, 143mpancom 650 . 2  |-  ( ph  ->  R  =  ( S  i^i  ( Y  X.  X ) ) )
14543, 144jca 518 1  |-  ( ph  ->  ( X  C_  Y  /\  R  =  ( S  i^i  ( Y  X.  X ) ) ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    <-> wb 176    /\ wa 358    /\ w3a 934    = wceq 1632    e. wcel 1696   A.wral 2556   _Vcvv 2801   [.wsbc 3004    i^i cin 3164    C_ wss 3165   {csn 3653   <.cop 3656   class class class wbr 4039   {copab 4092    _E cep 4319    We wwe 4367   Ord word 4407    X. cxp 4703   `'ccnv 4704   dom cdm 4705   ran crn 4706    |` cres 4707   "cima 4708   Rel wrel 4710   Fun wfun 5265    Fn wfn 5266   -->wf 5267   -onto->wfo 5269   -1-1-onto->wf1o 5270   ` cfv 5271    Isom wiso 5272  (class class class)co 5874  OrdIsocoi 7240
This theorem is referenced by:  fpwwe2lem10  8277
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-13 1698  ax-14 1700  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277  ax-rep 4147  ax-sep 4157  ax-nul 4165  ax-pow 4204  ax-pr 4230  ax-un 4528
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-eu 2160  df-mo 2161  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-ne 2461  df-ral 2561  df-rex 2562  df-reu 2563  df-rmo 2564  df-rab 2565  df-v 2803  df-sbc 3005  df-csb 3095  df-dif 3168  df-un 3170  df-in 3172  df-ss 3179  df-pss 3181  df-nul 3469  df-if 3579  df-pw 3640  df-sn 3659  df-pr 3660  df-tp 3661  df-op 3662  df-uni 3844  df-iun 3923  df-br 4040  df-opab 4094  df-mpt 4095  df-tr 4130  df-eprel 4321  df-id 4325  df-po 4330  df-so 4331  df-fr 4368  df-se 4369  df-we 4370  df-ord 4411  df-on 4412  df-lim 4413  df-suc 4414  df-xp 4711  df-rel 4712  df-cnv 4713  df-co 4714  df-dm 4715  df-rn 4716  df-res 4717  df-ima 4718  df-iota 5235  df-fun 5273  df-fn 5274  df-f 5275  df-f1 5276  df-fo 5277  df-f1o 5278  df-fv 5279  df-isom 5280  df-ov 5877  df-riota 6320  df-recs 6404  df-oi 7241
  Copyright terms: Public domain W3C validator