Users' Mathboxes Mathbox for Thierry Arnoux < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ordtrest2NEW Structured version   Unicode version

Theorem ordtrest2NEW 26351
Description: An interval-closed set  A in a total order has the same subspace topology as the restricted order topology. (An interval-closed set is the same thing as an open or half-open or closed interval in  RR, but in other sets like  QQ there are interval-closed sets like  ( pi , +oo )  i^i  QQ that are not intervals.) (Contributed by Mario Carneiro, 9-Sep-2015.) (Revised by Thierry Arnoux, 11-Sep-2018.)
Hypotheses
Ref Expression
ordtNEW.b  |-  B  =  ( Base `  K
)
ordtNEW.l  |-  .<_  =  ( ( le `  K
)  i^i  ( B  X.  B ) )
ordtrest2NEW.2  |-  ( ph  ->  K  e. Toset )
ordtrest2NEW.3  |-  ( ph  ->  A  C_  B )
ordtrest2NEW.4  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  ->  { z  e.  B  |  ( x  .<_  z  /\  z  .<_  y ) }  C_  A )
Assertion
Ref Expression
ordtrest2NEW  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  =  ( (ordTop `  .<_  )t  A ) )
Distinct variable groups:    x, y,  .<_    x, B, y    x, K, y    x, A, y, z    z,  .<_    z, A   
z, B    ph, x, y, z    z, K

Proof of Theorem ordtrest2NEW
Dummy variables  v  w are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ordtrest2NEW.2 . . . 4  |-  ( ph  ->  K  e. Toset )
2 tospos 26117 . . . 4  |-  ( K  e. Toset  ->  K  e.  Poset )
3 posprs 15117 . . . 4  |-  ( K  e.  Poset  ->  K  e.  Preset  )
41, 2, 33syl 20 . . 3  |-  ( ph  ->  K  e.  Preset  )
5 ordtrest2NEW.3 . . 3  |-  ( ph  ->  A  C_  B )
6 ordtNEW.b . . . 4  |-  B  =  ( Base `  K
)
7 ordtNEW.l . . . 4  |-  .<_  =  ( ( le `  K
)  i^i  ( B  X.  B ) )
86, 7ordtrestNEW 26349 . . 3  |-  ( ( K  e.  Preset  /\  A  C_  B )  ->  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  C_  ( (ordTop ` 
.<_  )t  A ) )
94, 5, 8syl2anc 661 . 2  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  C_  ( (ordTop `  .<_  )t  A ) )
10 eqid 2441 . . . . . . . 8  |-  ran  (
z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  =  ran  (
z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )
11 eqid 2441 . . . . . . . 8  |-  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
)  =  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
)
126, 7, 10, 11ordtprsval 26346 . . . . . . 7  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  =  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) ) ) )
134, 12syl 16 . . . . . 6  |-  ( ph  ->  (ordTop `  .<_  )  =  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) ) ) )
1413oveq1d 6104 . . . . 5  |-  ( ph  ->  ( (ordTop `  .<_  )t  A )  =  ( (
topGen `  ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) ) )t  A ) )
15 fibas 18580 . . . . . 6  |-  ( fi
`  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )  e.  TopBases
16 fvex 5699 . . . . . . . . 9  |-  ( Base `  K )  e.  _V
176, 16eqeltri 2511 . . . . . . . 8  |-  B  e. 
_V
1817a1i 11 . . . . . . 7  |-  ( ph  ->  B  e.  _V )
1918, 5ssexd 4437 . . . . . 6  |-  ( ph  ->  A  e.  _V )
20 tgrest 18761 . . . . . 6  |-  ( ( ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )  e.  TopBases  /\  A  e.  _V )  ->  ( topGen `  ( ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) )t  A ) )  =  ( ( topGen `  ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) ) )t  A ) )
2115, 19, 20sylancr 663 . . . . 5  |-  ( ph  ->  ( topGen `  ( ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )t  A ) )  =  ( ( topGen `  ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) ) )t  A ) )
2214, 21eqtr4d 2476 . . . 4  |-  ( ph  ->  ( (ordTop `  .<_  )t  A )  =  ( topGen `  ( ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) )t  A ) ) )
23 firest 14369 . . . . 5  |-  ( fi
`  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A ) )  =  ( ( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )t  A )
2423fveq2i 5692 . . . 4  |-  ( topGen `  ( fi `  (
( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )t  A ) ) )  =  ( topGen `  (
( fi `  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )t  A ) )
2522, 24syl6eqr 2491 . . 3  |-  ( ph  ->  ( (ordTop `  .<_  )t  A )  =  ( topGen `  ( fi `  (
( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )t  A ) ) ) )
26 fvex 5699 . . . . . . . . 9  |-  ( le
`  K )  e. 
_V
2726inex1 4431 . . . . . . . 8  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
287, 27eqeltri 2511 . . . . . . 7  |-  .<_  e.  _V
2928inex1 4431 . . . . . 6  |-  (  .<_  i^i  ( A  X.  A
) )  e.  _V
3029a1i 11 . . . . 5  |-  ( ph  ->  (  .<_  i^i  ( A  X.  A ) )  e.  _V )
31 ordttop 18802 . . . . 5  |-  ( ( 
.<_  i^i  ( A  X.  A ) )  e. 
_V  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e. 
Top )
3230, 31syl 16 . . . 4  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e. 
Top )
336, 7, 10, 11ordtprsuni 26347 . . . . . . . . 9  |-  ( K  e.  Preset  ->  B  =  U. ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) )
344, 33syl 16 . . . . . . . 8  |-  ( ph  ->  B  =  U. ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) )
3534, 18eqeltrrd 2516 . . . . . . 7  |-  ( ph  ->  U. ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  e. 
_V )
36 uniexb 6384 . . . . . . 7  |-  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  e.  _V  <->  U. ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  e. 
_V )
3735, 36sylibr 212 . . . . . 6  |-  ( ph  ->  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  e.  _V )
38 restval 14363 . . . . . 6  |-  ( ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  e.  _V  /\  A  e.  _V )  ->  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A )  =  ran  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) ) )
3937, 19, 38syl2anc 661 . . . . 5  |-  ( ph  ->  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A )  =  ran  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) ) )
40 dfss1 3553 . . . . . . . . . . . 12  |-  ( A 
C_  B  <->  ( B  i^i  A )  =  A )
415, 40sylib 196 . . . . . . . . . . 11  |-  ( ph  ->  ( B  i^i  A
)  =  A )
42 eqid 2441 . . . . . . . . . . . . . . 15  |-  dom  (  .<_  i^i  ( A  X.  A ) )  =  dom  (  .<_  i^i  ( A  X.  A ) )
4342ordttopon 18795 . . . . . . . . . . . . . 14  |-  ( ( 
.<_  i^i  ( A  X.  A ) )  e. 
_V  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e.  (TopOn `  dom  (  .<_  i^i  ( A  X.  A
) ) ) )
4430, 43syl 16 . . . . . . . . . . . . 13  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e.  (TopOn `  dom  (  .<_  i^i  ( A  X.  A
) ) ) )
456, 7prsssdm 26345 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Preset  /\  A  C_  B )  ->  dom  (  .<_  i^i  ( A  X.  A ) )  =  A )
464, 5, 45syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ph  ->  dom  (  .<_  i^i  ( A  X.  A ) )  =  A )
4746fveq2d 5693 . . . . . . . . . . . . 13  |-  ( ph  ->  (TopOn `  dom  (  .<_  i^i  ( A  X.  A
) ) )  =  (TopOn `  A )
)
4844, 47eleqtrd 2517 . . . . . . . . . . . 12  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e.  (TopOn `  A )
)
49 toponmax 18531 . . . . . . . . . . . 12  |-  ( (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  e.  (TopOn `  A )  ->  A  e.  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) )
5048, 49syl 16 . . . . . . . . . . 11  |-  ( ph  ->  A  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
5141, 50eqeltrd 2515 . . . . . . . . . 10  |-  ( ph  ->  ( B  i^i  A
)  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
52 elsni 3900 . . . . . . . . . . . 12  |-  ( v  e.  { B }  ->  v  =  B )
5352ineq1d 3549 . . . . . . . . . . 11  |-  ( v  e.  { B }  ->  ( v  i^i  A
)  =  ( B  i^i  A ) )
5453eleq1d 2507 . . . . . . . . . 10  |-  ( v  e.  { B }  ->  ( ( v  i^i 
A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  <->  ( B  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) ) )
5551, 54syl5ibrcom 222 . . . . . . . . 9  |-  ( ph  ->  ( v  e.  { B }  ->  ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) ) )
5655ralrimiv 2796 . . . . . . . 8  |-  ( ph  ->  A. v  e.  { B }  ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
57 ordtrest2NEW.4 . . . . . . . . . 10  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  ->  { z  e.  B  |  ( x  .<_  z  /\  z  .<_  y ) }  C_  A )
586, 7, 1, 5, 57ordtrest2NEWlem 26350 . . . . . . . . 9  |-  ( ph  ->  A. v  e.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } ) ( v  i^i 
A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
59 eqid 2441 . . . . . . . . . . . 12  |-  (ODual `  K )  =  (ODual `  K )
6059, 6odubas 15301 . . . . . . . . . . 11  |-  B  =  ( Base `  (ODual `  K ) )
617cnveqi 5012 . . . . . . . . . . . 12  |-  `'  .<_  =  `' ( ( le
`  K )  i^i  ( B  X.  B
) )
62 cnvin 5242 . . . . . . . . . . . . 13  |-  `' ( ( le `  K
)  i^i  ( B  X.  B ) )  =  ( `' ( le
`  K )  i^i  `' ( B  X.  B ) )
63 cnvxp 5253 . . . . . . . . . . . . . 14  |-  `' ( B  X.  B )  =  ( B  X.  B )
6463ineq2i 3547 . . . . . . . . . . . . 13  |-  ( `' ( le `  K
)  i^i  `' ( B  X.  B ) )  =  ( `' ( le `  K )  i^i  ( B  X.  B ) )
65 eqid 2441 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  =  ( le `  K
)
6659, 65oduleval 15299 . . . . . . . . . . . . . 14  |-  `' ( le `  K )  =  ( le `  (ODual `  K ) )
6766ineq1i 3546 . . . . . . . . . . . . 13  |-  ( `' ( le `  K
)  i^i  ( B  X.  B ) )  =  ( ( le `  (ODual `  K ) )  i^i  ( B  X.  B ) )
6862, 64, 673eqtri 2465 . . . . . . . . . . . 12  |-  `' ( ( le `  K
)  i^i  ( B  X.  B ) )  =  ( ( le `  (ODual `  K ) )  i^i  ( B  X.  B ) )
6961, 68eqtri 2461 . . . . . . . . . . 11  |-  `'  .<_  =  ( ( le `  (ODual `  K ) )  i^i  ( B  X.  B ) )
7059odutos 26122 . . . . . . . . . . . 12  |-  ( K  e. Toset  ->  (ODual `  K
)  e. Toset )
711, 70syl 16 . . . . . . . . . . 11  |-  ( ph  ->  (ODual `  K )  e. Toset )
72 vex 2973 . . . . . . . . . . . . . . . . . . 19  |-  y  e. 
_V
73 vex 2973 . . . . . . . . . . . . . . . . . . 19  |-  z  e. 
_V
7472, 73brcnv 5020 . . . . . . . . . . . . . . . . . 18  |-  ( y `'  .<_  z  <->  z  .<_  y )
75 vex 2973 . . . . . . . . . . . . . . . . . . 19  |-  x  e. 
_V
7673, 75brcnv 5020 . . . . . . . . . . . . . . . . . 18  |-  ( z `'  .<_  x  <->  x  .<_  z )
7774, 76anbi12ci 698 . . . . . . . . . . . . . . . . 17  |-  ( ( y `'  .<_  z  /\  z `'  .<_  x )  <-> 
( x  .<_  z  /\  z  .<_  y ) )
7877a1i 11 . . . . . . . . . . . . . . . 16  |-  ( z  e.  B  ->  (
( y `'  .<_  z  /\  z `'  .<_  x )  <->  ( x  .<_  z  /\  z  .<_  y ) ) )
7978rabbiia 2959 . . . . . . . . . . . . . . 15  |-  { z  e.  B  |  ( y `'  .<_  z  /\  z `'  .<_  x ) }  =  { z  e.  B  |  ( x  .<_  z  /\  z  .<_  y ) }
8079eqcomi 2445 . . . . . . . . . . . . . 14  |-  { z  e.  B  |  ( x  .<_  z  /\  z  .<_  y ) }  =  { z  e.  B  |  ( y `'  .<_  z  /\  z `'  .<_  x ) }
8180a1i 11 . . . . . . . . . . . . 13  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  ->  { z  e.  B  |  ( x  .<_  z  /\  z  .<_  y ) }  =  { z  e.  B  |  ( y `'  .<_  z  /\  z `'  .<_  x ) } )
8281, 57eqsstr3d 3389 . . . . . . . . . . . 12  |-  ( (
ph  /\  ( x  e.  A  /\  y  e.  A ) )  ->  { z  e.  B  |  ( y `' 
.<_  z  /\  z `'  .<_  x ) } 
C_  A )
8382ancom2s 800 . . . . . . . . . . 11  |-  ( (
ph  /\  ( y  e.  A  /\  x  e.  A ) )  ->  { z  e.  B  |  ( y `' 
.<_  z  /\  z `'  .<_  x ) } 
C_  A )
8460, 69, 71, 5, 83ordtrest2NEWlem 26350 . . . . . . . . . 10  |-  ( ph  ->  A. v  e.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  w `'  .<_  z } ) ( v  i^i  A )  e.  (ordTop `  ( `'  .<_  i^i  ( A  X.  A ) ) ) )
85 eqidd 2442 . . . . . . . . . . . . 13  |-  ( ph  ->  B  =  B )
86 vex 2973 . . . . . . . . . . . . . . . . . 18  |-  w  e. 
_V
8786, 73brcnv 5020 . . . . . . . . . . . . . . . . 17  |-  ( w `'  .<_  z  <->  z  .<_  w )
8887bicomi 202 . . . . . . . . . . . . . . . 16  |-  ( z 
.<_  w  <->  w `'  .<_  z )
8988a1i 11 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( z  .<_  w  <->  w `'  .<_  z ) )
9089notbid 294 . . . . . . . . . . . . . 14  |-  ( ph  ->  ( -.  z  .<_  w 
<->  -.  w `'  .<_  z ) )
9190rabbidv 2962 . . . . . . . . . . . . 13  |-  ( ph  ->  { w  e.  B  |  -.  z  .<_  w }  =  { w  e.  B  |  -.  w `'  .<_  z } )
9285, 91mpteq12dv 4368 . . . . . . . . . . . 12  |-  ( ph  ->  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
)  =  ( z  e.  B  |->  { w  e.  B  |  -.  w `'  .<_  z } ) )
9392rneqd 5065 . . . . . . . . . . 11  |-  ( ph  ->  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } )  =  ran  ( z  e.  B  |->  { w  e.  B  |  -.  w `'  .<_  z } ) )
94 cnvin 5242 . . . . . . . . . . . . . . 15  |-  `' ( 
.<_  i^i  ( A  X.  A ) )  =  ( `'  .<_  i^i  `' ( A  X.  A
) )
95 cnvxp 5253 . . . . . . . . . . . . . . . 16  |-  `' ( A  X.  A )  =  ( A  X.  A )
9695ineq2i 3547 . . . . . . . . . . . . . . 15  |-  ( `' 
.<_  i^i  `' ( A  X.  A ) )  =  ( `'  .<_  i^i  ( A  X.  A
) )
9794, 96eqtri 2461 . . . . . . . . . . . . . 14  |-  `' ( 
.<_  i^i  ( A  X.  A ) )  =  ( `'  .<_  i^i  ( A  X.  A ) )
9897fveq2i 5692 . . . . . . . . . . . . 13  |-  (ordTop `  `' (  .<_  i^i  ( A  X.  A ) ) )  =  (ordTop `  ( `'  .<_  i^i  ( A  X.  A ) ) )
996ressprs 26114 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Preset  /\  A  C_  B )  ->  ( Ks  A )  e.  Preset  )
1004, 5, 99syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ph  ->  ( Ks  A )  e.  Preset  )
101 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ( Base `  ( Ks  A ) )  =  ( Base `  ( Ks  A ) )
102 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ( ( le `  ( Ks  A ) )  i^i  (
( Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) )  =  ( ( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) )
103101, 102ordtcnvNEW 26348 . . . . . . . . . . . . . . 15  |-  ( ( Ks  A )  e.  Preset  -> 
(ordTop `  `' (
( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) ) )  =  (ordTop `  ( ( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) ) ) )
104100, 103syl 16 . . . . . . . . . . . . . 14  |-  ( ph  ->  (ordTop `  `' (
( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) ) )  =  (ordTop `  ( ( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) ) ) )
1056, 7prsss 26344 . . . . . . . . . . . . . . . . . 18  |-  ( ( K  e.  Preset  /\  A  C_  B )  ->  (  .<_  i^i  ( A  X.  A ) )  =  ( ( le `  K )  i^i  ( A  X.  A ) ) )
1064, 5, 105syl2anc 661 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  (  .<_  i^i  ( A  X.  A ) )  =  ( ( le
`  K )  i^i  ( A  X.  A
) ) )
107 eqid 2441 . . . . . . . . . . . . . . . . . . . 20  |-  ( Ks  A )  =  ( Ks  A )
108107, 65ressle 14336 . . . . . . . . . . . . . . . . . . 19  |-  ( A  e.  _V  ->  ( le `  K )  =  ( le `  ( Ks  A ) ) )
10919, 108syl 16 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( le `  K
)  =  ( le
`  ( Ks  A ) ) )
110107, 6ressbas2 14227 . . . . . . . . . . . . . . . . . . . 20  |-  ( A 
C_  B  ->  A  =  ( Base `  ( Ks  A ) ) )
1115, 110syl 16 . . . . . . . . . . . . . . . . . . 19  |-  ( ph  ->  A  =  ( Base `  ( Ks  A ) ) )
112111, 111xpeq12d 4863 . . . . . . . . . . . . . . . . . 18  |-  ( ph  ->  ( A  X.  A
)  =  ( (
Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) )
113109, 112ineq12d 3551 . . . . . . . . . . . . . . . . 17  |-  ( ph  ->  ( ( le `  K )  i^i  ( A  X.  A ) )  =  ( ( le
`  ( Ks  A ) )  i^i  ( (
Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) ) )
114106, 113eqtrd 2473 . . . . . . . . . . . . . . . 16  |-  ( ph  ->  (  .<_  i^i  ( A  X.  A ) )  =  ( ( le
`  ( Ks  A ) )  i^i  ( (
Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) ) )
115114cnveqd 5013 . . . . . . . . . . . . . . 15  |-  ( ph  ->  `' (  .<_  i^i  ( A  X.  A ) )  =  `' ( ( le `  ( Ks  A ) )  i^i  (
( Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) ) )
116115fveq2d 5693 . . . . . . . . . . . . . 14  |-  ( ph  ->  (ordTop `  `' (  .<_  i^i  ( A  X.  A ) ) )  =  (ordTop `  `' ( ( le `  ( Ks  A ) )  i^i  ( ( Base `  ( Ks  A ) )  X.  ( Base `  ( Ks  A ) ) ) ) ) )
117114fveq2d 5693 . . . . . . . . . . . . . 14  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  =  (ordTop `  ( ( le `  ( Ks  A ) )  i^i  ( (
Base `  ( Ks  A
) )  X.  ( Base `  ( Ks  A ) ) ) ) ) )
118104, 116, 1173eqtr4d 2483 . . . . . . . . . . . . 13  |-  ( ph  ->  (ordTop `  `' (  .<_  i^i  ( A  X.  A ) ) )  =  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
11998, 118syl5reqr 2488 . . . . . . . . . . . 12  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  =  (ordTop `  ( `'  .<_  i^i  ( A  X.  A ) ) ) )
120119eleq2d 2508 . . . . . . . . . . 11  |-  ( ph  ->  ( ( v  i^i 
A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  <->  ( v  i^i 
A )  e.  (ordTop `  ( `'  .<_  i^i  ( A  X.  A ) ) ) ) )
12193, 120raleqbidv 2929 . . . . . . . . . 10  |-  ( ph  ->  ( A. v  e. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  <->  A. v  e.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  w `'  .<_  z } ) ( v  i^i  A )  e.  (ordTop `  ( `'  .<_  i^i  ( A  X.  A ) ) ) ) )
12284, 121mpbird 232 . . . . . . . . 9  |-  ( ph  ->  A. v  e.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ( v  i^i 
A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
123 ralunb 3535 . . . . . . . . 9  |-  ( A. v  e.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  <->  ( A. v  e.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } ) ( v  i^i  A
)  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  /\  A. v  e. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) ) )
12458, 122, 123sylanbrc 664 . . . . . . . 8  |-  ( ph  ->  A. v  e.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ( v  i^i  A
)  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
125 ralunb 3535 . . . . . . . 8  |-  ( A. v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  <-> 
( A. v  e. 
{ B }  (
v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  /\  A. v  e.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) ) )
12656, 124, 125sylanbrc 664 . . . . . . 7  |-  ( ph  ->  A. v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) ( v  i^i 
A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
127 eqid 2441 . . . . . . . 8  |-  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) )  =  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) )
128127fmpt 5862 . . . . . . 7  |-  ( A. v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) ( v  i^i  A )  e.  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  <-> 
( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  |->  ( v  i^i 
A ) ) : ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) --> (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
129126, 128sylib 196 . . . . . 6  |-  ( ph  ->  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u. 
ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  |->  ( v  i^i 
A ) ) : ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) ) --> (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
130 frn 5563 . . . . . 6  |-  ( ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) ) : ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) ) --> (ordTop `  (  .<_  i^i  ( A  X.  A ) ) )  ->  ran  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )  |->  ( v  i^i  A ) )  C_  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
131129, 130syl 16 . . . . 5  |-  ( ph  ->  ran  ( v  e.  ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  ( z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w } ) ) )  |->  ( v  i^i  A ) ) 
C_  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) )
13239, 131eqsstrd 3388 . . . 4  |-  ( ph  ->  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A ) 
C_  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) )
133 tgfiss 18594 . . . 4  |-  ( ( (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  e. 
Top  /\  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A ) 
C_  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) ) )  ->  ( topGen `  ( fi `  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A ) ) )  C_  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
13432, 132, 133syl2anc 661 . . 3  |-  ( ph  ->  ( topGen `  ( fi `  ( ( { B }  u.  ( ran  ( z  e.  B  |->  { w  e.  B  |  -.  w  .<_  z } )  u.  ran  (
z  e.  B  |->  { w  e.  B  |  -.  z  .<_  w }
) ) )t  A ) ) )  C_  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
13525, 134eqsstrd 3388 . 2  |-  ( ph  ->  ( (ordTop `  .<_  )t  A )  C_  (ordTop `  (  .<_  i^i  ( A  X.  A ) ) ) )
1369, 135eqssd 3371 1  |-  ( ph  ->  (ordTop `  (  .<_  i^i  ( A  X.  A
) ) )  =  ( (ordTop `  .<_  )t  A ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2713   {crab 2717   _Vcvv 2970    u. cun 3324    i^i cin 3325    C_ wss 3326   {csn 3875   U.cuni 4089   class class class wbr 4290    e. cmpt 4348    X. cxp 4836   `'ccnv 4837   dom cdm 4838   ran crn 4839   -->wf 5412   ` cfv 5416  (class class class)co 6089   ficfi 7658   Basecbs 14172   ↾s cress 14173   lecple 14243   ↾t crest 14357   topGenctg 14374  ordTopcordt 14435    Preset cpreset 15094   Posetcpo 15108  Tosetctos 15201  ODualcodu 15296   Topctop 18496  TopOnctopon 18497   TopBasesctb 18500
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2422  ax-rep 4401  ax-sep 4411  ax-nul 4419  ax-pow 4468  ax-pr 4529  ax-un 6370  ax-cnex 9336  ax-resscn 9337  ax-1cn 9338  ax-icn 9339  ax-addcl 9340  ax-addrcl 9341  ax-mulcl 9342  ax-mulrcl 9343  ax-mulcom 9344  ax-addass 9345  ax-mulass 9346  ax-distr 9347  ax-i2m1 9348  ax-1ne0 9349  ax-1rid 9350  ax-rnegex 9351  ax-rrecex 9352  ax-cnre 9353  ax-pre-lttri 9354  ax-pre-lttrn 9355  ax-pre-ltadd 9356  ax-pre-mulgt0 9357
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-nel 2607  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3185  df-csb 3287  df-dif 3329  df-un 3331  df-in 3333  df-ss 3340  df-pss 3342  df-nul 3636  df-if 3790  df-pw 3860  df-sn 3876  df-pr 3878  df-tp 3880  df-op 3882  df-uni 4090  df-int 4127  df-iun 4171  df-iin 4172  df-br 4291  df-opab 4349  df-mpt 4350  df-tr 4384  df-eprel 4630  df-id 4634  df-po 4639  df-so 4640  df-fr 4677  df-we 4679  df-ord 4720  df-on 4721  df-lim 4722  df-suc 4723  df-xp 4844  df-rel 4845  df-cnv 4846  df-co 4847  df-dm 4848  df-rn 4849  df-res 4850  df-ima 4851  df-iota 5379  df-fun 5418  df-fn 5419  df-f 5420  df-f1 5421  df-fo 5422  df-f1o 5423  df-fv 5424  df-riota 6050  df-ov 6092  df-oprab 6093  df-mpt2 6094  df-om 6475  df-1st 6575  df-2nd 6576  df-recs 6830  df-rdg 6864  df-1o 6918  df-oadd 6922  df-er 7099  df-en 7309  df-dom 7310  df-sdom 7311  df-fin 7312  df-fi 7659  df-pnf 9418  df-mnf 9419  df-xr 9420  df-ltxr 9421  df-le 9422  df-sub 9595  df-neg 9596  df-nn 10321  df-2 10378  df-3 10379  df-4 10380  df-5 10381  df-6 10382  df-7 10383  df-8 10384  df-9 10385  df-10 10386  df-ndx 14175  df-slot 14176  df-base 14177  df-sets 14178  df-ress 14179  df-ple 14256  df-rest 14359  df-topgen 14380  df-ordt 14437  df-preset 15096  df-poset 15114  df-toset 15202  df-odu 15297  df-top 18501  df-bases 18503  df-topon 18504
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator