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

Theorem ordtconlem1 28569
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 28570. See also reconnlem1 21755. (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 1754 . . . . 5  |-  F/ r ( K  e. Toset  /\  A  C_  B )
2 nfcv 2591 . . . . . . 7  |-  F/_ r A
3 nfra2 2819 . . . . . . 7  |-  F/ r A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
42, 3nfral 2818 . . . . . 6  |-  F/ r A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
54nfn 1958 . . . . 5  |-  F/ r  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x 
.<_  r  /\  r  .<_  y )  ->  r  e.  A )
61, 5nfan 1986 . . . 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 28257 . . . . . . . . . 10  |-  ( K  e. Toset  ->  K  e.  Poset )
8 posprs 16145 . . . . . . . . . 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 5891 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  e. 
_V
1211inex1 4566 . . . . . . . . . . . . . 14  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
1310, 12eqeltri 2513 . . . . . . . . . . . . 13  |-  .<_  e.  _V
14 eqid 2429 . . . . . . . . . . . . . 14  |-  dom  .<_  =  dom  .<_
1514ordttopon 20140 . . . . . . . . . . . . 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 28559 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  dom  .<_  =  B )
1918fveq2d 5885 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  (TopOn `  dom  .<_  )  =  (TopOn `  B
) )
2016, 19syl5eleq 2523 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  e.  (TopOn `  B )
)
219, 20syl5eqel 2521 . . . . . . . . . 10  |-  ( K  e.  Preset  ->  J  e.  (TopOn `  B ) )
227, 8, 213syl 18 . . . . . . . . 9  |-  ( K  e. Toset  ->  J  e.  (TopOn `  B ) )
2322ad3antrrr 734 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
2423adantlr 719 . . . . . . 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 767 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  B )
2625adantlr 719 . . . . . . 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 758 . . . . . . . . . . . 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 4663 . . . . . . . . . . . . . . . 16  |-  { B }  e.  _V
30 fvex 5891 . . . . . . . . . . . . . . . . . . . 20  |-  ( Base `  K )  e.  _V
3117, 30eqeltri 2513 . . . . . . . . . . . . . . . . . . 19  |-  B  e. 
_V
3231mptex 6151 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  e.  _V
3332rnex 6741 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  e.  _V
3431mptex 6151 . . . . . . . . . . . . . . . . . 18  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3534rnex 6741 . . . . . . . . . . . . . . . . 17  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3633, 35unex 6603 . . . . . . . . . . . . . . . 16  |-  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  e.  _V
3729, 36unex 6603 . . . . . . . . . . . . . . 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 7939 . . . . . . . . . . . . . . 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 5891 . . . . . . . . . . . . . . 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 19912 . . . . . . . . . . . . . . 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 3479 . . . . . . . . . . . . 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 2429 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)
45 eqid 2429 . . . . . . . . . . . . . . 15  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
4617, 10, 44, 45ordtprsval 28563 . . . . . . . . . . . . . 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 2482 . . . . . . . . . . . . 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 3519 . . . . . . . . . . . 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 3650 . . . . . . . . . . 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 3650 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  C_  J )
52 breq2 4430 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
r  .<_  z  <->  r  .<_  y ) )
5352notbid 295 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  r  .<_  z  <->  -.  r  .<_  y ) )
5453cbvrabv 3086 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y }
55 breq1 4429 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
x  .<_  y  <->  r  .<_  y ) )
5655notbid 295 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  x  .<_  y  <->  -.  r  .<_  y ) )
5756rabbidv 3079 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  x  .<_  y }  =  { y  e.  B  |  -.  r  .<_  y } )
5857eqeq2d 2443 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y }  <->  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } ) )
5958rspcev 3188 . . . . . . . . . . . 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 675 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6131rabex 4576 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  r  .<_  z }  e.  _V
62 eqid 2429 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
6362elrnmpt 5101 . . . . . . . . . . . 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 215 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6665adantl 467 . . . . . . . . 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 3471 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6867ad2antrr 730 . . . . . . 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 3649 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  C_  J )
70 breq1 4429 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  (
z  .<_  r  <->  y  .<_  r ) )
7170notbid 295 . . . . . . . . . . . . 13  |-  ( z  =  y  ->  ( -.  z  .<_  r  <->  -.  y  .<_  r ) )
7271cbvrabv 3086 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r }
73 breq2 4430 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  (
y  .<_  x  <->  y  .<_  r ) )
7473notbid 295 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  ( -.  y  .<_  x  <->  -.  y  .<_  r ) )
7574rabbidv 3079 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  { y  e.  B  |  -.  y  .<_  x }  =  { y  e.  B  |  -.  y  .<_  r } )
7675eqeq2d 2443 . . . . . . . . . . . . 13  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }  <->  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } ) )
7776rspcev 3188 . . . . . . . . . . . 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 675 . . . . . . . . . . 11  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }
)
7931rabex 4576 . . . . . . . . . . . 12  |-  { z  e.  B  |  -.  z  .<_  r }  e.  _V
80 eqid 2429 . . . . . . . . . . . . 13  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )
8180elrnmpt 5101 . . . . . . . . . . . 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 215 . . . . . . . . . 10  |-  ( r  e.  B  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8483adantl 467 . . . . . . . . 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 3471 . . . . . . . 8  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8685ad2antrr 730 . . . . . . 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 758 . . . . . . . . 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 462 . . . . . . . . 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 534 . . . . . . . 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 768 . . . . . . . 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 3464 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
9291ancrd 556 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
x  e.  A  -> 
( x  e.  B  /\  x  e.  A
) ) )
9392anim1d 566 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  r  .<_  x )  ->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) ) )
9493impl 624 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  (
( x  e.  B  /\  x  e.  A
)  /\  -.  r  .<_  x ) )
95 elin 3655 . . . . . . . . . . . . 13  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( x  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A
) )
96 breq2 4430 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  (
r  .<_  z  <->  r  .<_  x ) )
9796notbid 295 . . . . . . . . . . . . . . 15  |-  ( z  =  x  ->  ( -.  r  .<_  z  <->  -.  r  .<_  x ) )
9897elrab 3235 . . . . . . . . . . . . . 14  |-  ( x  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( x  e.  B  /\  -.  r  .<_  x ) )
9998anbi1i 699 . . . . . . . . . . . . 13  |-  ( ( x  e.  { z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A )  <->  ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
) )
100 an32 805 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
)  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10195, 99, 1003bitri 274 . . . . . . . . . . . 12  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
10294, 101sylibr 215 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A
) )
103 ne0i 3773 . . . . . . . . . . 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 654 . . . . . . . . 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 2976 . . . . . . . 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 665 . . . . . . 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 769 . . . . . . . 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 3464 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
110109ancrd 556 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
( y  e.  B  /\  y  e.  A
) ) )
111110anim1d 566 . . . . . . . . . . . . 13  |-  ( A 
C_  B  ->  (
( y  e.  A  /\  -.  y  .<_  r )  ->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) ) )
112111impl 624 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  (
( y  e.  B  /\  y  e.  A
)  /\  -.  y  .<_  r ) )
113 elin 3655 . . . . . . . . . . . . 13  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( y  e. 
{ z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A
) )
11471elrab 3235 . . . . . . . . . . . . . 14  |-  ( y  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( y  e.  B  /\  -.  y  .<_  r ) )
115114anbi1i 699 . . . . . . . . . . . . 13  |-  ( ( y  e.  { z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A )  <->  ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
) )
116 an32 805 . . . . . . . . . . . . 13  |-  ( ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
)  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
117113, 115, 1163bitri 274 . . . . . . . . . . . 12  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
118112, 117sylibr 215 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A
) )
119 ne0i 3773 . . . . . . . . . . 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 654 . . . . . . . . 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 2976 . . . . . . . 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 665 . . . . . . 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 28265 . . . . . . . . . . . . . . . 16  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  (
r  .<_  z  \/  z  .<_  r ) )
125 oran 498 . . . . . . . . . . . . . . . 16  |-  ( ( r  .<_  z  \/  z  .<_  r )  <->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
126124, 125sylib 199 . . . . . . . . . . . . . . 15  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
1271263expa 1205 . . . . . . . . . . . . . 14  |-  ( ( ( K  e. Toset  /\  r  e.  B )  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
128127nrexdv 2888 . . . . . . . . . . . . 13  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  -.  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
129 rabid 3012 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( z  e.  B  /\  -.  r  .<_  z ) )
130 rabid 3012 . . . . . . . . . . . . . . . . . 18  |-  ( z  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( z  e.  B  /\  -.  z  .<_  r ) )
131129, 130anbi12i 701 . . . . . . . . . . . . . . . . 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 3655 . . . . . . . . . . . . . . . . 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 835 . . . . . . . . . . . . . . . . 17  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  /\  ( z  e.  B  /\  -.  z  .<_  r ) ) )
134131, 132, 1333bitr4i 280 . . . . . . . . . . . . . . . 16  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
135134exbii 1714 . . . . . . . . . . . . . . 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 3016 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  r  .<_  z }
137 nfrab1 3016 . . . . . . . . . . . . . . . . 17  |-  F/_ z { z  e.  B  |  -.  z  .<_  r }
138136, 137nfin 3675 . . . . . . . . . . . . . . . 16  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )
139138n0f 3776 . . . . . . . . . . . . . . 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 2788 . . . . . . . . . . . . . . 15  |-  ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  E. z ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
141135, 139, 1403bitr4i 280 . . . . . . . . . . . . . 14  |-  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
142141necon1bbii 2695 . . . . . . . . . . . . 13  |-  ( -. 
E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
143128, 142sylib 199 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
144143adantlr 719 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
145144adantr 466 . . . . . . . . . 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 3669 . . . . . . . . 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 3661 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (
(/)  i^i  A )
148 in0 3794 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (/)
149147, 148eqtr3i 2460 . . . . . . . . 9  |-  ( (/)  i^i 
A )  =  (/)
150146, 149syl6eq 2486 . . . . . . . 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 719 . . . . . . 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 760 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  r  e.  B )
153 simpr 462 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  -.  r  e.  A )
154 vex 3090 . . . . . . . . . . . . . . 15  |-  r  e. 
_V
155154snss 4127 . . . . . . . . . . . . . 14  |-  ( r  e.  B  <->  { r }  C_  B )
156 eldif 3452 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  ( r  e.  B  /\  -.  r  e.  A ) )
157154snss 4127 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  { r }  C_  ( B  \  A ) )
158156, 157bitr3i 254 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  B  /\  -.  r  e.  A
)  <->  { r }  C_  ( B  \  A ) )
159 ssconb 3604 . . . . . . . . . . . . . . 15  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( {
r }  C_  ( B  \  A )  <->  A  C_  ( B  \  { r } ) ) )
160158, 159syl5bb 260 . . . . . . . . . . . . . 14  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( (
r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
161155, 160sylanb 474 . . . . . . . . . . . . 13  |-  ( ( r  e.  B  /\  A  C_  B )  -> 
( ( r  e.  B  /\  -.  r  e.  A )  <->  A  C_  ( B  \  { r } ) ) )
162161adantl 467 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  (
r  e.  B  /\  A  C_  B ) )  ->  ( ( r  e.  B  /\  -.  r  e.  A )  <->  A 
C_  ( B  \  { r } ) ) )
163162anass1rs 814 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
164163adantr 466 . . . . . . . . . 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 929 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( B  \  {
r } ) )
1667ad3antrrr 734 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  K  e.  Poset )
167 nfv 1754 . . . . . . . . . . 11  |-  F/ z ( K  e.  Poset  /\  r  e.  B )
168136, 137nfun 3628 . . . . . . . . . . 11  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } )
169 nfcv 2591 . . . . . . . . . . 11  |-  F/_ z
( B  \  {
r } )
170 ianor 490 . . . . . . . . . . . . . . 15  |-  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )
17117, 10posrasymb 28256 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  r  =  z ) )
172 equcom 1846 . . . . . . . . . . . . . . . . 17  |-  ( r  =  z  <->  z  =  r )
173171, 172syl6bb 264 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  z  =  r ) )
174173necon3bbid 2678 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  z  =/=  r ) )
175170, 174syl5bbr 262 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) )
1761753expia 1207 . . . . . . . . . . . . 13  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  B  -> 
( ( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) ) )
177176pm5.32d 643 . . . . . . . . . . . 12  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( z  e.  B  /\  z  =/=  r ) ) )
178129, 130orbi12i 523 . . . . . . . . . . . . 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 3612 . . . . . . . . . . . . 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 875 . . . . . . . . . . . . 13  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  \/  ( z  e.  B  /\  -.  z  .<_  r ) ) )
181178, 179, 1803bitr4ri 281 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } ) )
182 eldifsn 4128 . . . . . . . . . . . . 13  |-  ( z  e.  ( B  \  { r } )  <-> 
( z  e.  B  /\  z  =/=  r
) )
183182bicomi 205 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  z  =/=  r )  <->  z  e.  ( B  \  { r } ) )
184177, 181, 1833bitr3g 290 . . . . . . . . . . 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 3488 . . . . . . . . . 10  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
186166, 152, 185syl2anc 665 . . . . . . . . 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 3507 . . . . . . . 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 719 . . . . . . 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 20369 . . . . . 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 651 . . . . 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 723 . . . 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 2885 . . . . . . . . . . 11  |-  ( E. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
193192rexbii 2934 . . . . . . . . . 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 2997 . . . . . . . . . 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 2880 . . . . . . . . . 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 278 . . . . . . . . 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 2934 . . . . . . . 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 2997 . . . . . . . 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 2880 . . . . . . . 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 278 . . . . . . 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 2987 . . . . . . . . . 10  |-  ( E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
202201rexbii 2934 . . . . . . . . 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 2987 . . . . . . . . 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 3003 . . . . . . . . . 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 699 . . . . . . . . 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 274 . . . . . . . 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 2934 . . . . . . 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 254 . . . . . 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 730 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e. Toset )
21025sselda 3470 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  B )
211 simpllr 767 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  r  e.  B )
21217, 10trleile 28265 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  x  e.  B  /\  r  e.  B )  ->  (
x  .<_  r  \/  r  .<_  x ) )
213209, 210, 211, 212syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  \/  r  .<_  x ) )
214 simpr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  A )
215 simplr 760 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  r  e.  A )
216 nelne2 2761 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  -.  r  e.  A
)  ->  x  =/=  r )
217214, 215, 216syl2anc 665 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  =/=  r )
218166adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e.  Poset
)
21917, 10posrasymb 28256 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  (
( x  .<_  r  /\  r  .<_  x )  <->  x  =  r ) )
220219necon3bbid 2678 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
221218, 210, 211, 220syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
222217, 221mpbird 235 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  (
x  .<_  r  /\  r  .<_  x ) )
223213, 222jca 534 . . . . . . . . . . . 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 896 . . . . . . . . . . . 12  |-  ( ( ( x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) )  <->  ( x  .<_  r  <->  -.  r  .<_  x ) )
225223, 224sylib 199 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  <->  -.  r  .<_  x ) )
226225rexbidva 2943 . . . . . . . . . 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 730 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e. Toset )
228 simpllr 767 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  e.  B )
22925sselda 3470 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  B )
23017, 10trleile 28265 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  r  e.  B  /\  y  e.  B )  ->  (
r  .<_  y  \/  y  .<_  r ) )
231227, 228, 229, 230syl3anc 1264 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  \/  y  .<_  r ) )
232 simpr 462 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  A )
233 simplr 760 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  r  e.  A )
234 nelne2 2761 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  r  e.  A
)  ->  y  =/=  r )
235232, 233, 234syl2anc 665 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  =/=  r )
236235necomd 2702 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  =/=  y )
237166adantr 466 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e.  Poset
)
23817, 10posrasymb 28256 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  (
( r  .<_  y  /\  y  .<_  r )  <->  r  =  y ) )
239238necon3bbid 2678 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
240237, 228, 229, 239syl3anc 1264 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
241236, 240mpbird 235 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  (
r  .<_  y  /\  y  .<_  r ) )
242231, 241jca 534 . . . . . . . . . . . 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 896 . . . . . . . . . . . 12  |-  ( ( ( r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) )  <->  ( r  .<_  y 
<->  -.  y  .<_  r ) )
244242, 243sylib 199 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  <->  -.  y  .<_  r ) )
245244rexbidva 2943 . . . . . . . . . 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 715 . . . . . . . . 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 435 . . . . . . . 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 644 . . . . . . 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 2943 . . . . . 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 260 . . . . 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 486 . . . 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 2975 . . 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 435 . 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 108 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 187    \/ wo 369    /\ wa 370    /\ w3a 982    = wceq 1437   E.wex 1659    e. wcel 1870    =/= wne 2625   A.wral 2782   E.wrex 2783   {crab 2786   _Vcvv 3087    \ cdif 3439    u. cun 3440    i^i cin 3441    C_ wss 3442   (/)c0 3767   {csn 4002   class class class wbr 4426    |-> cmpt 4484    X. cxp 4852   dom cdm 4854   ran crn 4855   ` cfv 5601  (class class class)co 6305   ficfi 7930   Basecbs 15084   lecple 15159   ↾t crest 15278   topGenctg 15295  ordTopcordt 15356    Preset cpreset 16122   Posetcpo 16136  Tosetctos 16230  TopOnctopon 19849   Conccon 20357
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-8 1872  ax-9 1874  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407  ax-rep 4538  ax-sep 4548  ax-nul 4556  ax-pow 4603  ax-pr 4661  ax-un 6597
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3or 983  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-eu 2270  df-mo 2271  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ne 2627  df-ral 2787  df-rex 2788  df-reu 2789  df-rab 2791  df-v 3089  df-sbc 3306  df-csb 3402  df-dif 3445  df-un 3447  df-in 3449  df-ss 3456  df-pss 3458  df-nul 3768  df-if 3916  df-pw 3987  df-sn 4003  df-pr 4005  df-tp 4007  df-op 4009  df-uni 4223  df-int 4259  df-iun 4304  df-br 4427  df-opab 4485  df-mpt 4486  df-tr 4521  df-eprel 4765  df-id 4769  df-po 4775  df-so 4776  df-fr 4813  df-we 4815  df-xp 4860  df-rel 4861  df-cnv 4862  df-co 4863  df-dm 4864  df-rn 4865  df-res 4866  df-ima 4867  df-pred 5399  df-ord 5445  df-on 5446  df-lim 5447  df-suc 5448  df-iota 5565  df-fun 5603  df-fn 5604  df-f 5605  df-f1 5606  df-fo 5607  df-f1o 5608  df-fv 5609  df-ov 6308  df-oprab 6309  df-mpt2 6310  df-om 6707  df-1st 6807  df-2nd 6808  df-wrecs 7036  df-recs 7098  df-rdg 7136  df-1o 7190  df-oadd 7194  df-er 7371  df-en 7578  df-fin 7581  df-fi 7931  df-rest 15280  df-topgen 15301  df-ordt 15358  df-preset 16124  df-poset 16142  df-toset 16231  df-top 19852  df-bases 19853  df-topon 19854  df-cld 19965  df-con 20358
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator