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

Theorem ordtconlem1 28730
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 28731. See also reconnlem1 21844. (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 1761 . . . . 5  |-  F/ r ( K  e. Toset  /\  A  C_  B )
2 nfcv 2592 . . . . . . 7  |-  F/_ r A
3 nfra2 2775 . . . . . . 7  |-  F/ r A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
42, 3nfral 2774 . . . . . 6  |-  F/ r A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
54nfn 1983 . . . . 5  |-  F/ r  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x 
.<_  r  /\  r  .<_  y )  ->  r  e.  A )
61, 5nfan 2011 . . . 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 28419 . . . . . . . . . 10  |-  ( K  e. Toset  ->  K  e.  Poset )
8 posprs 16194 . . . . . . . . . 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 5875 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  e. 
_V
1211inex1 4544 . . . . . . . . . . . . . 14  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
1310, 12eqeltri 2525 . . . . . . . . . . . . 13  |-  .<_  e.  _V
14 eqid 2451 . . . . . . . . . . . . . 14  |-  dom  .<_  =  dom  .<_
1514ordttopon 20209 . . . . . . . . . . . . 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 28720 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  dom  .<_  =  B )
1918fveq2d 5869 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  (TopOn `  dom  .<_  )  =  (TopOn `  B
) )
2016, 19syl5eleq 2535 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  e.  (TopOn `  B )
)
219, 20syl5eqel 2533 . . . . . . . . . 10  |-  ( K  e.  Preset  ->  J  e.  (TopOn `  B ) )
227, 8, 213syl 18 . . . . . . . . 9  |-  ( K  e. Toset  ->  J  e.  (TopOn `  B ) )
2322ad3antrrr 736 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
2423adantlr 721 . . . . . . 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 769 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  B )
2625adantlr 721 . . . . . . 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 760 . . . . . . . . . . . 12  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e. Toset )
2827, 7, 83syl 18 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e.  Preset  )
29 snex 4641 . . . . . . . . . . . . . . . 16  |-  { B }  e.  _V
30 fvex 5875 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  K )  e.  _V
3117, 30eqeltri 2525 . . . . . . . . . . . . . . . . . . 19  |-  B  e. 
_V
3231mptex 6136 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  e.  _V
3332rnex 6727 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  e.  _V
3431mptex 6136 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3534rnex 6727 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3633, 35unex 6589 . . . . . . . . . . . . . . . 16  |-  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  e.  _V
3729, 36unex 6589 . . . . . . . . . . . . . . 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 7933 . . . . . . . . . . . . . . 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 5875 . . . . . . . . . . . . . . 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 19981 . . . . . . . . . . . . . . 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 3441 . . . . . . . . . . . . 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 2451 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)
45 eqid 2451 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
4617, 10, 44, 45ordtprsval 28724 . . . . . . . . . . . . . 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 2497 . . . . . . . . . . . . 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 3481 . . . . . . . . . . . 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 3612 . . . . . . . . . . 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 17 . . . . . . . . . 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 3612 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  C_  J )
52 breq2 4406 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
r  .<_  z  <->  r  .<_  y ) )
5352notbid 296 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  r  .<_  z  <->  -.  r  .<_  y ) )
5453cbvrabv 3044 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y }
55 breq1 4405 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
x  .<_  y  <->  r  .<_  y ) )
5655notbid 296 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  x  .<_  y  <->  -.  r  .<_  y ) )
5756rabbidv 3036 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  x  .<_  y }  =  { y  e.  B  |  -.  r  .<_  y } )
5857eqeq2d 2461 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y }  <->  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } ) )
5958rspcev 3150 . . . . . . . . . . . 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 677 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6131rabex 4554 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  e.  _V
62 eqid 2451 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
6362elrnmpt 5081 . . . . . . . . . . . 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 216 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6665adantl 468 . . . . . . . . 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 3433 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6867ad2antrr 732 . . . . . . 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 3611 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  C_  J )
70 breq1 4405 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
z  .<_  r  <->  y  .<_  r ) )
7170notbid 296 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  z  .<_  r  <->  -.  y  .<_  r ) )
7271cbvrabv 3044 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r }
73 breq2 4406 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
y  .<_  x  <->  y  .<_  r ) )
7473notbid 296 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  y  .<_  x  <->  -.  y  .<_  r ) )
7574rabbidv 3036 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  y  .<_  x }  =  { y  e.  B  |  -.  y  .<_  r } )
7675eqeq2d 2461 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }  <->  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } ) )
7776rspcev 3150 . . . . . . . . . . . 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 677 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }
)
7931rabex 4554 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  e.  _V
80 eqid 2451 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )
8180elrnmpt 5081 . . . . . . . . . . . 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 216 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8483adantl 468 . . . . . . . . 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 3433 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8685ad2antrr 732 . . . . . . 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 760 . . . . . . . . 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 463 . . . . . . . . 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 535 . . . . . . . 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 770 . . . . . . . 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 3426 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
9291ancrd 557 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
x  e.  A  -> 
( x  e.  B  /\  x  e.  A
) ) )
9392anim1d 568 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  r  .<_  x )  ->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) ) )
9493impl 626 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  (
( x  e.  B  /\  x  e.  A
)  /\  -.  r  .<_  x ) )
95 elin 3617 . . . . . . . . . . . . 13  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( x  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A
) )
96 breq2 4406 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  (
r  .<_  z  <->  r  .<_  x ) )
9796notbid 296 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  ( -.  r  .<_  z  <->  -.  r  .<_  x ) )
9897elrab 3196 . . . . . . . . . . . . . 14  |-  ( x  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( x  e.  B  /\  -.  r  .<_  x ) )
9998anbi1i 701 . . . . . . . . . . . . 13  |-  ( ( x  e.  { z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A )  <->  ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
) )
100 an32 807 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
)  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10195, 99, 1003bitri 275 . . . . . . . . . . . 12  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10294, 101sylibr 216 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A
) )
103 ne0i 3737 . . . . . . . . . . 11  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  ->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
104102, 103syl 17 . . . . . . . . . 10  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
10525, 104sylanl1 656 . . . . . . . . 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 2931 . . . . . . . 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 667 . . . . . . 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 771 . . . . . . . 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 3426 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
110109ancrd 557 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
( y  e.  B  /\  y  e.  A
) ) )
111110anim1d 568 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( y  e.  A  /\  -.  y  .<_  r )  ->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) ) )
112111impl 626 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  (
( y  e.  B  /\  y  e.  A
)  /\  -.  y  .<_  r ) )
113 elin 3617 . . . . . . . . . . . . 13  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( y  e. 
{ z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A
) )
11471elrab 3196 . . . . . . . . . . . . . 14  |-  ( y  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( y  e.  B  /\  -.  y  .<_  r ) )
115114anbi1i 701 . . . . . . . . . . . . 13  |-  ( ( y  e.  { z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A )  <->  ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
) )
116 an32 807 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
)  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
117113, 115, 1163bitri 275 . . . . . . . . . . . 12  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
118112, 117sylibr 216 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A
) )
119 ne0i 3737 . . . . . . . . . . 11  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  ->  ( {
z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
120118, 119syl 17 . . . . . . . . . 10  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
12125, 120sylanl1 656 . . . . . . . . 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 2931 . . . . . . . 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 667 . . . . . . 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 28427 . . . . . . . . . . . . . . . 16  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  (
r  .<_  z  \/  z  .<_  r ) )
125 oran 499 . . . . . . . . . . . . . . . 16  |-  ( ( r  .<_  z  \/  z  .<_  r )  <->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
126124, 125sylib 200 . . . . . . . . . . . . . . 15  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
1271263expa 1208 . . . . . . . . . . . . . 14  |-  ( ( ( K  e. Toset  /\  r  e.  B )  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
128127nrexdv 2843 . . . . . . . . . . . . 13  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  -.  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
129 rabid 2967 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( z  e.  B  /\  -.  r  .<_  z ) )
130 rabid 2967 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( z  e.  B  /\  -.  z  .<_  r ) )
131129, 130anbi12i 703 . . . . . . . . . . . . . . . . 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 3617 . . . . . . . . . . . . . . . . 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 837 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  /\  ( z  e.  B  /\  -.  z  .<_  r ) ) )
134131, 132, 1333bitr4i 281 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
135134exbii 1718 . . . . . . . . . . . . . . 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 2971 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  r  .<_  z }
137 nfrab1 2971 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  z  .<_  r }
138136, 137nfin 3639 . . . . . . . . . . . . . . . 16  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )
139138n0f 3740 . . . . . . . . . . . . . . 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 2743 . . . . . . . . . . . . . . 15  |-  ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  E. z ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
141135, 139, 1403bitr4i 281 . . . . . . . . . . . . . 14  |-  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
142141necon1bbii 2673 . . . . . . . . . . . . 13  |-  ( -. 
E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
143128, 142sylib 200 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
144143adantlr 721 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
145144adantr 467 . . . . . . . . . 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 3633 . . . . . . . . 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 3625 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (
(/)  i^i  A )
148 in0 3760 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (/)
149147, 148eqtr3i 2475 . . . . . . . . 9  |-  ( (/)  i^i 
A )  =  (/)
150146, 149syl6eq 2501 . . . . . . . 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 721 . . . . . . 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 762 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  r  e.  B )
153 simpr 463 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  -.  r  e.  A )
154 vex 3048 . . . . . . . . . . . . . . 15  |-  r  e. 
_V
155154snss 4096 . . . . . . . . . . . . . 14  |-  ( r  e.  B  <->  { r }  C_  B )
156 eldif 3414 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  ( r  e.  B  /\  -.  r  e.  A ) )
157154snss 4096 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  { r }  C_  ( B  \  A ) )
158156, 157bitr3i 255 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  B  /\  -.  r  e.  A
)  <->  { r }  C_  ( B  \  A ) )
159 ssconb 3566 . . . . . . . . . . . . . . 15  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( {
r }  C_  ( B  \  A )  <->  A  C_  ( B  \  { r } ) ) )
160158, 159syl5bb 261 . . . . . . . . . . . . . 14  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( (
r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
161155, 160sylanb 475 . . . . . . . . . . . . 13  |-  ( ( r  e.  B  /\  A  C_  B )  -> 
( ( r  e.  B  /\  -.  r  e.  A )  <->  A  C_  ( B  \  { r } ) ) )
162161adantl 468 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  (
r  e.  B  /\  A  C_  B ) )  ->  ( ( r  e.  B  /\  -.  r  e.  A )  <->  A 
C_  ( B  \  { r } ) ) )
163162anass1rs 816 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
164163adantr 467 . . . . . . . . . 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 932 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( B  \  {
r } ) )
1667ad3antrrr 736 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  K  e.  Poset )
167 nfv 1761 . . . . . . . . . . 11  |-  F/ z ( K  e.  Poset  /\  r  e.  B )
168136, 137nfun 3590 . . . . . . . . . . 11  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } )
169 nfcv 2592 . . . . . . . . . . 11  |-  F/_ z
( B  \  {
r } )
170 ianor 491 . . . . . . . . . . . . . . 15  |-  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )
17117, 10posrasymb 28418 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  r  =  z ) )
172 equcom 1862 . . . . . . . . . . . . . . . . 17  |-  ( r  =  z  <->  z  =  r )
173171, 172syl6bb 265 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  z  =  r ) )
174173necon3bbid 2661 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  z  =/=  r ) )
175170, 174syl5bbr 263 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) )
1761753expia 1210 . . . . . . . . . . . . 13  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  B  -> 
( ( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) ) )
177176pm5.32d 645 . . . . . . . . . . . 12  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( z  e.  B  /\  z  =/=  r ) ) )
178129, 130orbi12i 524 . . . . . . . . . . . . 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 3574 . . . . . . . . . . . . 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 878 . . . . . . . . . . . . 13  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  \/  ( z  e.  B  /\  -.  z  .<_  r ) ) )
181178, 179, 1803bitr4ri 282 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } ) )
182 eldifsn 4097 . . . . . . . . . . . . 13  |-  ( z  e.  ( B  \  { r } )  <-> 
( z  e.  B  /\  z  =/=  r
) )
183182bicomi 206 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  z  =/=  r )  <->  z  e.  ( B  \  { r } ) )
184177, 181, 1833bitr3g 291 . . . . . . . . . . 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 3450 . . . . . . . . . 10  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
186166, 152, 185syl2anc 667 . . . . . . . . 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 3469 . . . . . . . 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 721 . . . . . . 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 20438 . . . . . 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 653 . . . . 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 725 . . . 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 2840 . . . . . . . . . . 11  |-  ( E. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
193192rexbii 2889 . . . . . . . . . 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 2952 . . . . . . . . . 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 2836 . . . . . . . . . 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 279 . . . . . . . . 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 2889 . . . . . . . 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 2952 . . . . . . . 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 2836 . . . . . . . 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 279 . . . . . . 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 2942 . . . . . . . . . 10  |-  ( E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
202201rexbii 2889 . . . . . . . . 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 2942 . . . . . . . . 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 2958 . . . . . . . . . 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 701 . . . . . . . . 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 275 . . . . . . . 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 2889 . . . . . . 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 255 . . . . . 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 732 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e. Toset )
21025sselda 3432 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  B )
211 simpllr 769 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  r  e.  B )
21217, 10trleile 28427 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  x  e.  B  /\  r  e.  B )  ->  (
x  .<_  r  \/  r  .<_  x ) )
213209, 210, 211, 212syl3anc 1268 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  \/  r  .<_  x ) )
214 simpr 463 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  A )
215 simplr 762 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  r  e.  A )
216 nelne2 2721 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  -.  r  e.  A
)  ->  x  =/=  r )
217214, 215, 216syl2anc 667 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  =/=  r )
218166adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e.  Poset
)
21917, 10posrasymb 28418 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  (
( x  .<_  r  /\  r  .<_  x )  <->  x  =  r ) )
220219necon3bbid 2661 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
221218, 210, 211, 220syl3anc 1268 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
222217, 221mpbird 236 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  (
x  .<_  r  /\  r  .<_  x ) )
223213, 222jca 535 . . . . . . . . . . . 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 899 . . . . . . . . . . . 12  |-  ( ( ( x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) )  <->  ( x  .<_  r  <->  -.  r  .<_  x ) )
225223, 224sylib 200 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  <->  -.  r  .<_  x ) )
226225rexbidva 2898 . . . . . . . . . 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 732 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e. Toset )
228 simpllr 769 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  e.  B )
22925sselda 3432 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  B )
23017, 10trleile 28427 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  r  e.  B  /\  y  e.  B )  ->  (
r  .<_  y  \/  y  .<_  r ) )
231227, 228, 229, 230syl3anc 1268 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  \/  y  .<_  r ) )
232 simpr 463 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  A )
233 simplr 762 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  r  e.  A )
234 nelne2 2721 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  r  e.  A
)  ->  y  =/=  r )
235232, 233, 234syl2anc 667 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  =/=  r )
236235necomd 2679 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  =/=  y )
237166adantr 467 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e.  Poset
)
23817, 10posrasymb 28418 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  (
( r  .<_  y  /\  y  .<_  r )  <->  r  =  y ) )
239238necon3bbid 2661 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
240237, 228, 229, 239syl3anc 1268 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
241236, 240mpbird 236 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  (
r  .<_  y  /\  y  .<_  r ) )
242231, 241jca 535 . . . . . . . . . . . 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 899 . . . . . . . . . . . 12  |-  ( ( ( r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) )  <->  ( r  .<_  y 
<->  -.  y  .<_  r ) )
244242, 243sylib 200 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  <->  -.  y  .<_  r ) )
245244rexbidva 2898 . . . . . . . . . 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 717 . . . . . . . . 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 436 . . . . . . . 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 646 . . . . . . 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 2898 . . . . . 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 261 . . . . 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 487 . . . 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 2930 . . 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 436 . 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 109 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 188    \/ wo 370    /\ wa 371    /\ w3a 985    = wceq 1444   E.wex 1663    e. wcel 1887    =/= wne 2622   A.wral 2737   E.wrex 2738   {crab 2741   _Vcvv 3045    \ cdif 3401    u. cun 3402    i^i cin 3403    C_ wss 3404   (/)c0 3731   {csn 3968   class class class wbr 4402    |-> cmpt 4461    X. cxp 4832   dom cdm 4834   ran crn 4835   ` cfv 5582  (class class class)co 6290   ficfi 7924   Basecbs 15121   lecple 15197   ↾t crest 15319   topGenctg 15336  ordTopcordt 15397    Preset cpreset 16171   Posetcpo 16185  Tosetctos 16279  TopOnctopon 19918   Conccon 20426
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-8 1889  ax-9 1896  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431  ax-rep 4515  ax-sep 4525  ax-nul 4534  ax-pow 4581  ax-pr 4639  ax-un 6583
This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-3or 986  df-3an 987  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-eu 2303  df-mo 2304  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ne 2624  df-ral 2742  df-rex 2743  df-reu 2744  df-rab 2746  df-v 3047  df-sbc 3268  df-csb 3364  df-dif 3407  df-un 3409  df-in 3411  df-ss 3418  df-pss 3420  df-nul 3732  df-if 3882  df-pw 3953  df-sn 3969  df-pr 3971  df-tp 3973  df-op 3975  df-uni 4199  df-int 4235  df-iun 4280  df-br 4403  df-opab 4462  df-mpt 4463  df-tr 4498  df-eprel 4745  df-id 4749  df-po 4755  df-so 4756  df-fr 4793  df-we 4795  df-xp 4840  df-rel 4841  df-cnv 4842  df-co 4843  df-dm 4844  df-rn 4845  df-res 4846  df-ima 4847  df-pred 5380  df-ord 5426  df-on 5427  df-lim 5428  df-suc 5429  df-iota 5546  df-fun 5584  df-fn 5585  df-f 5586  df-f1 5587  df-fo 5588  df-f1o 5589  df-fv 5590  df-ov 6293  df-oprab 6294  df-mpt2 6295  df-om 6693  df-1st 6793  df-2nd 6794  df-wrecs 7028  df-recs 7090  df-rdg 7128  df-1o 7182  df-oadd 7186  df-er 7363  df-en 7570  df-fin 7573  df-fi 7925  df-rest 15321  df-topgen 15342  df-ordt 15399  df-preset 16173  df-poset 16191  df-toset 16280  df-top 19921  df-bases 19922  df-topon 19923  df-cld 20034  df-con 20427
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator