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

Theorem ordtconlem1 27779
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 27780. See also reconnlem1 21204. (Contributed by Thierry Arnoux, 14-Sep-2018.)
Hypotheses
Ref Expression
ordtcon.x  |-  B  =  ( Base `  K
)
ordtcon.l  |-  .<_  =  ( ( le `  K
)  i^i  ( B  X.  B ) )
ordtcon.j  |-  J  =  (ordTop `  .<_  )
Assertion
Ref Expression
ordtconlem1  |-  ( ( K  e. Toset  /\  A  C_  B )  ->  (
( Jt  A )  e.  Con  ->  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) ) )
Distinct variable groups:    x, r,
y, A    B, r, x, y    J, r    K, r, x, y    x,  .<_ , y
Allowed substitution hints:    J( x, y)    .<_ ( r)

Proof of Theorem ordtconlem1
Dummy variable  z is distinct from all other variables.
StepHypRef Expression
1 nfv 1694 . . . . 5  |-  F/ r ( K  e. Toset  /\  A  C_  B )
2 nfcv 2605 . . . . . . 7  |-  F/_ r A
3 nfra2 2830 . . . . . . 7  |-  F/ r A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
42, 3nfral 2829 . . . . . 6  |-  F/ r A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
54nfn 1887 . . . . 5  |-  F/ r  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x 
.<_  r  /\  r  .<_  y )  ->  r  e.  A )
61, 5nfan 1914 . . . 4  |-  F/ r ( ( K  e. Toset  /\  A  C_  B )  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
7 tospos 27519 . . . . . . . . . 10  |-  ( K  e. Toset  ->  K  e.  Poset )
8 posprs 15452 . . . . . . . . . 10  |-  ( K  e.  Poset  ->  K  e.  Preset  )
9 ordtcon.j . . . . . . . . . . 11  |-  J  =  (ordTop `  .<_  )
10 ordtcon.l . . . . . . . . . . . . . 14  |-  .<_  =  ( ( le `  K
)  i^i  ( B  X.  B ) )
11 fvex 5866 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  e. 
_V
1211inex1 4578 . . . . . . . . . . . . . 14  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
1310, 12eqeltri 2527 . . . . . . . . . . . . 13  |-  .<_  e.  _V
14 eqid 2443 . . . . . . . . . . . . . 14  |-  dom  .<_  =  dom  .<_
1514ordttopon 19567 . . . . . . . . . . . . 13  |-  (  .<_  e.  _V  ->  (ordTop `  .<_  )  e.  (TopOn `  dom  .<_  ) )
1613, 15ax-mp 5 . . . . . . . . . . . 12  |-  (ordTop `  .<_  )  e.  (TopOn `  dom  .<_  )
17 ordtcon.x . . . . . . . . . . . . . 14  |-  B  =  ( Base `  K
)
1817, 10prsdm 27769 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  dom  .<_  =  B )
1918fveq2d 5860 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  (TopOn `  dom  .<_  )  =  (TopOn `  B
) )
2016, 19syl5eleq 2537 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  e.  (TopOn `  B )
)
219, 20syl5eqel 2535 . . . . . . . . . 10  |-  ( K  e.  Preset  ->  J  e.  (TopOn `  B ) )
227, 8, 213syl 20 . . . . . . . . 9  |-  ( K  e. Toset  ->  J  e.  (TopOn `  B ) )
2322ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
2423adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
25 simpllr 760 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  B )
2625adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  A  C_  B )
27 simpll 753 . . . . . . . . . . . 12  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e. Toset )
2827, 7, 83syl 20 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e.  Preset  )
29 snex 4678 . . . . . . . . . . . . . . . 16  |-  { B }  e.  _V
30 fvex 5866 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  K )  e.  _V
3117, 30eqeltri 2527 . . . . . . . . . . . . . . . . . . 19  |-  B  e. 
_V
3231mptex 6128 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  e.  _V
3332rnex 6719 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  e.  _V
3431mptex 6128 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3534rnex 6719 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3633, 35unex 6583 . . . . . . . . . . . . . . . 16  |-  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  e.  _V
3729, 36unex 6583 . . . . . . . . . . . . . . 15  |-  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  e. 
_V
38 ssfii 7881 . . . . . . . . . . . . . . 15  |-  ( ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u. 
ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  e.  _V  ->  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u. 
ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  C_  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) )
3937, 38ax-mp 5 . . . . . . . . . . . . . 14  |-  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  C_  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) )
40 fvex 5866 . . . . . . . . . . . . . . 15  |-  ( fi
`  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) )  e.  _V
41 bastg 19340 . . . . . . . . . . . . . . 15  |-  ( ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) )  e.  _V  ->  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) 
C_  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) ) )
4240, 41ax-mp 5 . . . . . . . . . . . . . 14  |-  ( fi
`  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) 
C_  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) )
4339, 42sstri 3498 . . . . . . . . . . . . 13  |-  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  C_  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) )
44 eqid 2443 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)
45 eqid 2443 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
4617, 10, 44, 45ordtprsval 27773 . . . . . . . . . . . . . 14  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  =  ( topGen `  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) ) )
479, 46syl5eq 2496 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  J  =  (
topGen `  ( fi `  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  u. 
ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) ) ) )
4843, 47syl5sseqr 3538 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  C_  J )
4948unssbd 3667 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  ( ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  C_  J
)
5028, 49syl 16 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  C_  J
)
5150unssbd 3667 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  C_  J )
52 breq2 4441 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
r  .<_  z  <->  r  .<_  y ) )
5352notbid 294 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  r  .<_  z  <->  -.  r  .<_  y ) )
5453cbvrabv 3094 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y }
55 breq1 4440 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
x  .<_  y  <->  r  .<_  y ) )
5655notbid 294 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  x  .<_  y  <->  -.  r  .<_  y ) )
5756rabbidv 3087 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  x  .<_  y }  =  { y  e.  B  |  -.  r  .<_  y } )
5857eqeq2d 2457 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y }  <->  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } ) )
5958rspcev 3196 . . . . . . . . . . . 12  |-  ( ( r  e.  B  /\  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } )  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6054, 59mpan2 671 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6131rabex 4588 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  e.  _V
62 eqid 2443 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
6362elrnmpt 5239 . . . . . . . . . . . 12  |-  ( { z  e.  B  |  -.  r  .<_  z }  e.  _V  ->  ( { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  <->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } ) )
6461, 63ax-mp 5 . . . . . . . . . . 11  |-  ( { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  <->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6560, 64sylibr 212 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6665adantl 466 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6751, 66sseldd 3490 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6867ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6950unssad 3666 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  C_  J )
70 breq1 4440 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
z  .<_  r  <->  y  .<_  r ) )
7170notbid 294 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  z  .<_  r  <->  -.  y  .<_  r ) )
7271cbvrabv 3094 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r }
73 breq2 4441 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
y  .<_  x  <->  y  .<_  r ) )
7473notbid 294 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  y  .<_  x  <->  -.  y  .<_  r ) )
7574rabbidv 3087 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  y  .<_  x }  =  { y  e.  B  |  -.  y  .<_  r } )
7675eqeq2d 2457 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }  <->  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } ) )
7776rspcev 3196 . . . . . . . . . . . 12  |-  ( ( r  e.  B  /\  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } )  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x } )
7872, 77mpan2 671 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }
)
7931rabex 4588 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  e.  _V
80 eqid 2443 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )
8180elrnmpt 5239 . . . . . . . . . . . 12  |-  ( { z  e.  B  |  -.  z  .<_  r }  e.  _V  ->  ( { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  <->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x } ) )
8279, 81ax-mp 5 . . . . . . . . . . 11  |-  ( { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  <->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x } )
8378, 82sylibr 212 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8483adantl 466 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8569, 84sseldd 3490 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8685ad2antrr 725 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
87 simpll 753 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( K  e. Toset  /\  A  C_  B )  /\  r  e.  B ) )
88 simpr 461 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  -.  r  e.  A )
8987, 88jca 532 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A ) )
90 simplrl 761 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  E. x  e.  A  -.  r  .<_  x )
91 ssel 3483 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
9291ancrd 554 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
x  e.  A  -> 
( x  e.  B  /\  x  e.  A
) ) )
9392anim1d 564 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  r  .<_  x )  ->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) ) )
9493impl 620 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  (
( x  e.  B  /\  x  e.  A
)  /\  -.  r  .<_  x ) )
95 elin 3672 . . . . . . . . . . . . 13  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( x  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A
) )
96 breq2 4441 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  (
r  .<_  z  <->  r  .<_  x ) )
9796notbid 294 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  ( -.  r  .<_  z  <->  -.  r  .<_  x ) )
9897elrab 3243 . . . . . . . . . . . . . 14  |-  ( x  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( x  e.  B  /\  -.  r  .<_  x ) )
9998anbi1i 695 . . . . . . . . . . . . 13  |-  ( ( x  e.  { z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A )  <->  ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
) )
100 an32 798 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
)  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10195, 99, 1003bitri 271 . . . . . . . . . . . 12  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10294, 101sylibr 212 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A
) )
103 ne0i 3776 . . . . . . . . . . 11  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  ->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
104102, 103syl 16 . . . . . . . . . 10  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
10525, 104sylanl1 650 . . . . . . . . 9  |-  ( ( ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
106105r19.29an 2984 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. x  e.  A  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
10789, 90, 106syl2anc 661 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
108 simplrr 762 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  E. y  e.  A  -.  y  .<_  r )
109 ssel 3483 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
110109ancrd 554 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
( y  e.  B  /\  y  e.  A
) ) )
111110anim1d 564 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( y  e.  A  /\  -.  y  .<_  r )  ->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) ) )
112111impl 620 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  (
( y  e.  B  /\  y  e.  A
)  /\  -.  y  .<_  r ) )
113 elin 3672 . . . . . . . . . . . . 13  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( y  e. 
{ z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A
) )
11471elrab 3243 . . . . . . . . . . . . . 14  |-  ( y  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( y  e.  B  /\  -.  y  .<_  r ) )
115114anbi1i 695 . . . . . . . . . . . . 13  |-  ( ( y  e.  { z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A )  <->  ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
) )
116 an32 798 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
)  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
117113, 115, 1163bitri 271 . . . . . . . . . . . 12  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
118112, 117sylibr 212 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A
) )
119 ne0i 3776 . . . . . . . . . . 11  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  ->  ( {
z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
120118, 119syl 16 . . . . . . . . . 10  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
12125, 120sylanl1 650 . . . . . . . . 9  |-  ( ( ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
122121r19.29an 2984 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. y  e.  A  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
12389, 108, 122syl2anc 661 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
12417, 10trleile 27527 . . . . . . . . . . . . . . . 16  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  (
r  .<_  z  \/  z  .<_  r ) )
125 oran 496 . . . . . . . . . . . . . . . 16  |-  ( ( r  .<_  z  \/  z  .<_  r )  <->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
126124, 125sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
1271263expa 1197 . . . . . . . . . . . . . 14  |-  ( ( ( K  e. Toset  /\  r  e.  B )  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
128127nrexdv 2899 . . . . . . . . . . . . 13  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  -.  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
129 rabid 3020 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( z  e.  B  /\  -.  r  .<_  z ) )
130 rabid 3020 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( z  e.  B  /\  -.  z  .<_  r ) )
131129, 130anbi12i 697 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  { z  e.  B  |  -.  r  .<_  z }  /\  z  e.  { z  e.  B  |  -.  z  .<_  r } )  <-> 
( ( z  e.  B  /\  -.  r  .<_  z )  /\  (
z  e.  B  /\  -.  z  .<_  r ) ) )
132 elin 3672 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  z  e.  {
z  e.  B  |  -.  z  .<_  r } ) )
133 anandi 828 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  /\  ( z  e.  B  /\  -.  z  .<_  r ) ) )
134131, 132, 1333bitr4i 277 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
135134exbii 1654 . . . . . . . . . . . . . . 15  |-  ( E. z  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  E. z
( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
136 nfrab1 3024 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  r  .<_  z }
137 nfrab1 3024 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  z  .<_  r }
138136, 137nfin 3690 . . . . . . . . . . . . . . . 16  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )
139138n0f 3779 . . . . . . . . . . . . . . 15  |-  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } ) )
140 df-rex 2799 . . . . . . . . . . . . . . 15  |-  ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  E. z ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
141135, 139, 1403bitr4i 277 . . . . . . . . . . . . . 14  |-  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
142141necon1bbii 2707 . . . . . . . . . . . . 13  |-  ( -. 
E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
143128, 142sylib 196 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
144143adantlr 714 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
145144adantr 465 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
146145ineq1d 3684 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )  i^i  A )  =  ( (/)  i^i  A
) )
147 incom 3676 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (
(/)  i^i  A )
148 in0 3797 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (/)
149147, 148eqtr3i 2474 . . . . . . . . 9  |-  ( (/)  i^i 
A )  =  (/)
150146, 149syl6eq 2500 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )  i^i  A )  =  (/) )
151150adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )  i^i  A )  =  (/) )
152 simplr 755 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  r  e.  B )
153 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  -.  r  e.  A )
154 vex 3098 . . . . . . . . . . . . . . 15  |-  r  e. 
_V
155154snss 4139 . . . . . . . . . . . . . 14  |-  ( r  e.  B  <->  { r }  C_  B )
156 eldif 3471 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  ( r  e.  B  /\  -.  r  e.  A ) )
157154snss 4139 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  { r }  C_  ( B  \  A ) )
158156, 157bitr3i 251 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  B  /\  -.  r  e.  A
)  <->  { r }  C_  ( B  \  A ) )
159 ssconb 3622 . . . . . . . . . . . . . . 15  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( {
r }  C_  ( B  \  A )  <->  A  C_  ( B  \  { r } ) ) )
160158, 159syl5bb 257 . . . . . . . . . . . . . 14  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( (
r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
161155, 160sylanb 472 . . . . . . . . . . . . 13  |-  ( ( r  e.  B  /\  A  C_  B )  -> 
( ( r  e.  B  /\  -.  r  e.  A )  <->  A  C_  ( B  \  { r } ) ) )
162161adantl 466 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  (
r  e.  B  /\  A  C_  B ) )  ->  ( ( r  e.  B  /\  -.  r  e.  A )  <->  A 
C_  ( B  \  { r } ) ) )
163162anass1rs 807 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
164163adantr 465 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
165152, 153, 164mpbi2and 921 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( B  \  {
r } ) )
1667ad3antrrr 729 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  K  e.  Poset )
167 nfv 1694 . . . . . . . . . . 11  |-  F/ z ( K  e.  Poset  /\  r  e.  B )
168136, 137nfun 3645 . . . . . . . . . . 11  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } )
169 nfcv 2605 . . . . . . . . . . 11  |-  F/_ z
( B  \  {
r } )
170 ianor 488 . . . . . . . . . . . . . . 15  |-  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )
17117, 10posrasymb 27518 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  r  =  z ) )
172 equcom 1780 . . . . . . . . . . . . . . . . 17  |-  ( r  =  z  <->  z  =  r )
173171, 172syl6bb 261 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  z  =  r ) )
174173necon3bbid 2690 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  z  =/=  r ) )
175170, 174syl5bbr 259 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) )
1761753expia 1199 . . . . . . . . . . . . 13  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  B  -> 
( ( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) ) )
177176pm5.32d 639 . . . . . . . . . . . 12  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( z  e.  B  /\  z  =/=  r ) ) )
178129, 130orbi12i 521 . . . . . . . . . . . . 13  |-  ( ( z  e.  { z  e.  B  |  -.  r  .<_  z }  \/  z  e.  { z  e.  B  |  -.  z  .<_  r } )  <-> 
( ( z  e.  B  /\  -.  r  .<_  z )  \/  (
z  e.  B  /\  -.  z  .<_  r ) ) )
179 elun 3630 . . . . . . . . . . . . 13  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e. 
{ z  e.  B  |  -.  r  .<_  z }  \/  z  e.  {
z  e.  B  |  -.  z  .<_  r } ) )
180 andi 867 . . . . . . . . . . . . 13  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  \/  ( z  e.  B  /\  -.  z  .<_  r ) ) )
181178, 179, 1803bitr4ri 278 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } ) )
182 eldifsn 4140 . . . . . . . . . . . . 13  |-  ( z  e.  ( B  \  { r } )  <-> 
( z  e.  B  /\  z  =/=  r
) )
183182bicomi 202 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  z  =/=  r )  <->  z  e.  ( B  \  { r } ) )
184177, 181, 1833bitr3g 287 . . . . . . . . . . 11  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  <->  z  e.  ( B  \  { r } ) ) )
185167, 168, 169, 184eqrd 3507 . . . . . . . . . 10  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
186166, 152, 185syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
187165, 186sseqtr4d 3526 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } ) )
188187adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  A  C_  ( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } ) )
18924, 26, 68, 86, 107, 123, 151, 188nconsubb 19797 . . . . . 6  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  -.  ( Jt  A )  e.  Con )
190189anasss 647 . . . . 5  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) )  ->  -.  ( Jt  A )  e.  Con )
191190adantllr 718 . . . 4  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )  /\  r  e.  B )  /\  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A )
)  ->  -.  ( Jt  A )  e.  Con )
192 rexanali 2896 . . . . . . . . . . 11  |-  ( E. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
193192rexbii 2945 . . . . . . . . . 10  |-  ( E. y  e.  A  E. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. y  e.  A  -.  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) )
194 rexcom 3005 . . . . . . . . . 10  |-  ( E. y  e.  A  E. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. r  e.  B  E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A ) )
195 rexnal 2891 . . . . . . . . . 10  |-  ( E. y  e.  A  -.  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  -> 
r  e.  A )  <->  -.  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) )
196193, 194, 1953bitr3i 275 . . . . . . . . 9  |-  ( E. r  e.  B  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. y  e.  A  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
197196rexbii 2945 . . . . . . . 8  |-  ( E. x  e.  A  E. r  e.  B  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. x  e.  A  -.  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) )
198 rexcom 3005 . . . . . . . 8  |-  ( E. x  e.  A  E. r  e.  B  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. r  e.  B  E. x  e.  A  E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A ) )
199 rexnal 2891 . . . . . . . 8  |-  ( E. x  e.  A  -.  A. y  e.  A  A. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  -> 
r  e.  A )  <->  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) )
200197, 198, 1993bitr3i 275 . . . . . . 7  |-  ( E. r  e.  B  E. x  e.  A  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
201 r19.41v 2995 . . . . . . . . . 10  |-  ( E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
202201rexbii 2945 . . . . . . . . 9  |-  ( E. x  e.  A  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. x  e.  A  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
) )
203 r19.41v 2995 . . . . . . . . 9  |-  ( E. x  e.  A  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. x  e.  A  E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
204 reeanv 3011 . . . . . . . . . 10  |-  ( E. x  e.  A  E. y  e.  A  (
x  .<_  r  /\  r  .<_  y )  <->  ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y ) )
205204anbi1i 695 . . . . . . . . 9  |-  ( ( E. x  e.  A  E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( ( E. x  e.  A  x 
.<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A ) )
206202, 203, 2053bitri 271 . . . . . . . 8  |-  ( E. x  e.  A  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( ( E. x  e.  A  x 
.<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A ) )
207206rexbii 2945 . . . . . . 7  |-  ( E. r  e.  B  E. x  e.  A  E. y  e.  A  (
( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. r  e.  B  ( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A ) )
208200, 207bitr3i 251 . . . . . 6  |-  ( -. 
A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)  <->  E. r  e.  B  ( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A ) )
20927ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e. Toset )
21025sselda 3489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  B )
211 simpllr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  r  e.  B )
21217, 10trleile 27527 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  x  e.  B  /\  r  e.  B )  ->  (
x  .<_  r  \/  r  .<_  x ) )
213209, 210, 211, 212syl3anc 1229 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  \/  r  .<_  x ) )
214 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  A )
215 simplr 755 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  r  e.  A )
216 nelne2 2773 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  -.  r  e.  A
)  ->  x  =/=  r )
217214, 215, 216syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  =/=  r )
218166adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e.  Poset
)
21917, 10posrasymb 27518 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  (
( x  .<_  r  /\  r  .<_  x )  <->  x  =  r ) )
220219necon3bbid 2690 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
221218, 210, 211, 220syl3anc 1229 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
222217, 221mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  (
x  .<_  r  /\  r  .<_  x ) )
223213, 222jca 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( (
x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) ) )
224 pm5.17 888 . . . . . . . . . . . 12  |-  ( ( ( x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) )  <->  ( x  .<_  r  <->  -.  r  .<_  x ) )
225223, 224sylib 196 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  <->  -.  r  .<_  x ) )
226225rexbidva 2951 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( E. x  e.  A  x  .<_  r  <->  E. x  e.  A  -.  r  .<_  x ) )
22727ad2antrr 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e. Toset )
228 simpllr 760 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  e.  B )
22925sselda 3489 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  B )
23017, 10trleile 27527 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  r  e.  B  /\  y  e.  B )  ->  (
r  .<_  y  \/  y  .<_  r ) )
231227, 228, 229, 230syl3anc 1229 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  \/  y  .<_  r ) )
232 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  A )
233 simplr 755 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  r  e.  A )
234 nelne2 2773 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  r  e.  A
)  ->  y  =/=  r )
235232, 233, 234syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  =/=  r )
236235necomd 2714 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  =/=  y )
237166adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e.  Poset
)
23817, 10posrasymb 27518 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  (
( r  .<_  y  /\  y  .<_  r )  <->  r  =  y ) )
239238necon3bbid 2690 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
240237, 228, 229, 239syl3anc 1229 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
241236, 240mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  (
r  .<_  y  /\  y  .<_  r ) )
242231, 241jca 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( (
r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) ) )
243 pm5.17 888 . . . . . . . . . . . 12  |-  ( ( ( r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) )  <->  ( r  .<_  y 
<->  -.  y  .<_  r ) )
244242, 243sylib 196 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  <->  -.  y  .<_  r ) )
245244rexbidva 2951 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( E. y  e.  A  r  .<_  y  <->  E. y  e.  A  -.  y  .<_  r ) )
246226, 245anbi12d 710 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r 
.<_  y )  <->  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) ) )
247246ex 434 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( -.  r  e.  A  ->  ( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  <-> 
( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) ) ) )
248247pm5.32rd 640 . . . . . . 7  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A )  <->  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) ) )
249248rexbidva 2951 . . . . . 6  |-  ( ( K  e. Toset  /\  A  C_  B )  ->  ( E. r  e.  B  ( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A )  <->  E. r  e.  B  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) ) )
250208, 249syl5bb 257 . . . . 5  |-  ( ( K  e. Toset  /\  A  C_  B )  ->  ( -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)  <->  E. r  e.  B  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A )
) )
251250biimpa 484 . . . 4  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  -> 
r  e.  A ) )  ->  E. r  e.  B  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) )
2526, 191, 251r19.29af 2983 . . 3  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  -> 
r  e.  A ) )  ->  -.  ( Jt  A )  e.  Con )
253252ex 434 . 2  |-  ( ( K  e. Toset  /\  A  C_  B )  ->  ( -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)  ->  -.  ( Jt  A )  e.  Con ) )
254253con4d 105 1  |-  ( ( K  e. Toset  /\  A  C_  B )  ->  (
( Jt  A )  e.  Con  ->  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) ) )
Colors of variables: wff setvar class
Syntax hints:   -. wn 3    -> wi 4    <-> wb 184    \/ wo 368    /\ wa 369    /\ w3a 974    = wceq 1383   E.wex 1599    e. wcel 1804    =/= wne 2638   A.wral 2793   E.wrex 2794   {crab 2797   _Vcvv 3095    \ cdif 3458    u. cun 3459    i^i cin 3460    C_ wss 3461   (/)c0 3770   {csn 4014   class class class wbr 4437    |-> cmpt 4495    X. cxp 4987   dom cdm 4989   ran crn 4990   ` cfv 5578  (class class class)co 6281   ficfi 7872   Basecbs 14509   lecple 14581   ↾t crest 14695   topGenctg 14712  ordTopcordt 14773    Preset cpreset 15429   Posetcpo 15443  Tosetctos 15537  TopOnctopon 19268   Conccon 19785
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-8 1806  ax-9 1808  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421  ax-rep 4548  ax-sep 4558  ax-nul 4566  ax-pow 4615  ax-pr 4676  ax-un 6577
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 975  df-3an 976  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-eu 2272  df-mo 2273  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-ne 2640  df-ral 2798  df-rex 2799  df-reu 2800  df-rab 2802  df-v 3097  df-sbc 3314  df-csb 3421  df-dif 3464  df-un 3466  df-in 3468  df-ss 3475  df-pss 3477  df-nul 3771  df-if 3927  df-pw 3999  df-sn 4015  df-pr 4017  df-tp 4019  df-op 4021  df-uni 4235  df-int 4272  df-iun 4317  df-br 4438  df-opab 4496  df-mpt 4497  df-tr 4531  df-eprel 4781  df-id 4785  df-po 4790  df-so 4791  df-fr 4828  df-we 4830  df-ord 4871  df-on 4872  df-lim 4873  df-suc 4874  df-xp 4995  df-rel 4996  df-cnv 4997  df-co 4998  df-dm 4999  df-rn 5000  df-res 5001  df-ima 5002  df-iota 5541  df-fun 5580  df-fn 5581  df-f 5582  df-f1 5583  df-fo 5584  df-f1o 5585  df-fv 5586  df-ov 6284  df-oprab 6285  df-mpt2 6286  df-om 6686  df-1st 6785  df-2nd 6786  df-recs 7044  df-rdg 7078  df-1o 7132  df-oadd 7136  df-er 7313  df-en 7519  df-fin 7522  df-fi 7873  df-rest 14697  df-topgen 14718  df-ordt 14775  df-preset 15431  df-poset 15449  df-toset 15538  df-top 19272  df-bases 19274  df-topon 19275  df-cld 19393  df-con 19786
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator