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

Theorem ordtconlem1 26274
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 26275. See also reconnlem1 20303. (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 1678 . . . . 5  |-  F/ r ( K  e. Toset  /\  A  C_  B )
2 nfcv 2577 . . . . . . 7  |-  F/_ r A
3 nfra1 2764 . . . . . . . 8  |-  F/ r A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
42, 3nfral 2767 . . . . . . 7  |-  F/ r A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
52, 4nfral 2767 . . . . . 6  |-  F/ r A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
65nfn 1840 . . . . 5  |-  F/ r  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x 
.<_  r  /\  r  .<_  y )  ->  r  e.  A )
71, 6nfan 1865 . . . 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 ) )
8 tospos 26036 . . . . . . . . . 10  |-  ( K  e. Toset  ->  K  e.  Poset )
9 posprs 15115 . . . . . . . . . 10  |-  ( K  e.  Poset  ->  K  e.  Preset  )
10 ordtcon.j . . . . . . . . . . 11  |-  J  =  (ordTop `  .<_  )
11 ordtcon.l . . . . . . . . . . . . . 14  |-  .<_  =  ( ( le `  K
)  i^i  ( B  X.  B ) )
12 fvex 5698 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  e. 
_V
1312inex1 4430 . . . . . . . . . . . . . 14  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
1411, 13eqeltri 2511 . . . . . . . . . . . . 13  |-  .<_  e.  _V
15 eqid 2441 . . . . . . . . . . . . . 14  |-  dom  .<_  =  dom  .<_
1615ordttopon 18697 . . . . . . . . . . . . 13  |-  (  .<_  e.  _V  ->  (ordTop `  .<_  )  e.  (TopOn `  dom  .<_  ) )
1714, 16ax-mp 5 . . . . . . . . . . . 12  |-  (ordTop `  .<_  )  e.  (TopOn `  dom  .<_  )
18 ordtcon.x . . . . . . . . . . . . . 14  |-  B  =  ( Base `  K
)
1918, 11prsdm 26264 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  dom  .<_  =  B )
2019fveq2d 5692 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  (TopOn `  dom  .<_  )  =  (TopOn `  B
) )
2117, 20syl5eleq 2527 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  e.  (TopOn `  B )
)
2210, 21syl5eqel 2525 . . . . . . . . . 10  |-  ( K  e.  Preset  ->  J  e.  (TopOn `  B ) )
238, 9, 223syl 20 . . . . . . . . 9  |-  ( K  e. Toset  ->  J  e.  (TopOn `  B ) )
2423ad3antrrr 724 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
2524adantlr 709 . . . . . . 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 )
)
26 simpllr 753 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  B )
2726adantlr 709 . . . . . . 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 )
28 simpll 748 . . . . . . . . . . . . 13  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e. Toset )
2928, 8, 93syl 20 . . . . . . . . . . . 12  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  K  e.  Preset  )
30 snex 4530 . . . . . . . . . . . . . . . . 17  |-  { B }  e.  _V
31 fvex 5698 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  K )  e.  _V
3218, 31eqeltri 2511 . . . . . . . . . . . . . . . . . . . 20  |-  B  e. 
_V
3332mptex 5945 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  e.  _V
3433rnex 6511 . . . . . . . . . . . . . . . . . 18  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  e.  _V
3532mptex 5945 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3635rnex 6511 . . . . . . . . . . . . . . . . . 18  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3734, 36unex 6377 . . . . . . . . . . . . . . . . 17  |-  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  e.  _V
3830, 37unex 6377 . . . . . . . . . . . . . . . 16  |-  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) )  e. 
_V
39 ssfii 7665 . . . . . . . . . . . . . . . 16  |-  ( ( { 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 } ) ) ) ) )
4038, 39ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( { 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 } ) ) ) )
41 fvex 5698 . . . . . . . . . . . . . . . 16  |-  ( fi
`  ( { B }  u.  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) ) ) )  e.  _V
42 bastg 18471 . . . . . . . . . . . . . . . 16  |-  ( ( 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 } ) ) ) ) ) )
4341, 42ax-mp 5 . . . . . . . . . . . . . . 15  |-  ( 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 } ) ) ) ) )
4440, 43sstri 3362 . . . . . . . . . . . . . 14  |-  ( { 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 } ) ) ) ) )
45 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)
46 eqid 2441 . . . . . . . . . . . . . . . 16  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
4718, 11, 45, 46ordtprsval 26268 . . . . . . . . . . . . . . 15  |-  ( 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 } ) ) ) ) ) )
4810, 47syl5eq 2485 . . . . . . . . . . . . . 14  |-  ( 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 } ) ) ) ) ) )
4944, 48syl5sseqr 3402 . . . . . . . . . . . . 13  |-  ( 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 )
5049unssbd 3531 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  ( ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  C_  J
)
5129, 50syl 16 . . . . . . . . . . 11  |-  ( ( ( 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
)
5251unssbd 3531 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  C_  J )
53 breq2 4293 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
r  .<_  z  <->  r  .<_  y ) )
5453notbid 294 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  ( -.  r  .<_  z  <->  -.  r  .<_  y ) )
5554cbvrabv 2969 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y }
56 breq1 4292 . . . . . . . . . . . . . . . . 17  |-  ( x  =  r  ->  (
x  .<_  y  <->  r  .<_  y ) )
5756notbid 294 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  ( -.  x  .<_  y  <->  -.  r  .<_  y ) )
5857rabbidv 2962 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  { y  e.  B  |  -.  x  .<_  y }  =  { y  e.  B  |  -.  r  .<_  y } )
5958eqeq2d 2452 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y }  <->  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } ) )
6059rspcev 3070 . . . . . . . . . . . . 13  |-  ( ( 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 } )
6155, 60mpan2 666 . . . . . . . . . . . 12  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6232rabex 4440 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  r  .<_  z }  e.  _V
63 eqid 2441 . . . . . . . . . . . . . 14  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
6463elrnmpt 5082 . . . . . . . . . . . . 13  |-  ( { 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 } ) )
6562, 64ax-mp 5 . . . . . . . . . . . 12  |-  ( { 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 } )
6661, 65sylibr 212 . . . . . . . . . . 11  |-  ( r  e.  B  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6766adantl 463 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )
6852, 67sseldd 3354 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6968adantr 462 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
7069adantlr 709 . . . . . . 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 )
7151unssad 3530 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  C_  J )
72 breq1 4292 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
z  .<_  r  <->  y  .<_  r ) )
7372notbid 294 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  ( -.  z  .<_  r  <->  -.  y  .<_  r ) )
7473cbvrabv 2969 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r }
75 breq2 4293 . . . . . . . . . . . . . . . . 17  |-  ( x  =  r  ->  (
y  .<_  x  <->  y  .<_  r ) )
7675notbid 294 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  ( -.  y  .<_  x  <->  -.  y  .<_  r ) )
7776rabbidv 2962 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  { y  e.  B  |  -.  y  .<_  x }  =  { y  e.  B  |  -.  y  .<_  r } )
7877eqeq2d 2452 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }  <->  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } ) )
7978rspcev 3070 . . . . . . . . . . . . 13  |-  ( ( 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 } )
8074, 79mpan2 666 . . . . . . . . . . . 12  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }
)
8132rabex 4440 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  z  .<_  r }  e.  _V
82 eqid 2441 . . . . . . . . . . . . . 14  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )
8382elrnmpt 5082 . . . . . . . . . . . . 13  |-  ( { 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 } ) )
8481, 83ax-mp 5 . . . . . . . . . . . 12  |-  ( { 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 } )
8580, 84sylibr 212 . . . . . . . . . . 11  |-  ( r  e.  B  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8685adantl 463 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
) )
8771, 86sseldd 3354 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8887adantr 462 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8988adantlr 709 . . . . . . 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 )
90 simpll 748 . . . . . . . . 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 ) )
91 simpr 458 . . . . . . . . 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 )
9290, 91jca 529 . . . . . . . 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 ) )
93 simplr 749 . . . . . . . . 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 )  ->  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )
9493simpld 456 . . . . . . . 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 )
95 nfv 1678 . . . . . . . . . 10  |-  F/ x
( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )
96 nfre1 2770 . . . . . . . . . 10  |-  F/ x E. x  e.  A  -.  r  .<_  x
9795, 96nfan 1865 . . . . . . . . 9  |-  F/ x
( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. x  e.  A  -.  r  .<_  x )
98 ssel 3347 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
9998ancrd 551 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
x  e.  A  -> 
( x  e.  B  /\  x  e.  A
) ) )
10099anim1d 561 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  r  .<_  x )  ->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) ) )
101100impl 617 . . . . . . . . . . . . 13  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  (
( x  e.  B  /\  x  e.  A
)  /\  -.  r  .<_  x ) )
102 elin 3536 . . . . . . . . . . . . . 14  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( x  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A
) )
103 breq2 4293 . . . . . . . . . . . . . . . . 17  |-  ( z  =  x  ->  (
r  .<_  z  <->  r  .<_  x ) )
104103notbid 294 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  ( -.  r  .<_  z  <->  -.  r  .<_  x ) )
105104elrab 3114 . . . . . . . . . . . . . . 15  |-  ( x  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( x  e.  B  /\  -.  r  .<_  x ) )
106105anbi1i 690 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A )  <->  ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
) )
107 an32 791 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
)  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
108102, 106, 1073bitri 271 . . . . . . . . . . . . 13  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) )
109101, 108sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A
) )
110 ne0i 3640 . . . . . . . . . . . 12  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  ->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
111109, 110syl 16 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
11226, 111sylanl1 645 . . . . . . . . . 10  |-  ( ( ( ( ( ( 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 )  =/=  (/) )
113112adantllr 713 . . . . . . . . 9  |-  ( ( ( ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. x  e.  A  -.  r  .<_  x )  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
114 simpr 458 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. x  e.  A  -.  r  .<_  x )  ->  E. x  e.  A  -.  r  .<_  x )
11597, 113, 114r19.29af 2859 . . . . . . . 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 )  =/=  (/) )
11692, 94, 115syl2anc 656 . . . . . . 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 )  =/=  (/) )
11793simprd 460 . . . . . . . 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 )
118 nfv 1678 . . . . . . . . . 10  |-  F/ y ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )
119 nfre1 2770 . . . . . . . . . 10  |-  F/ y E. y  e.  A  -.  y  .<_  r
120118, 119nfan 1865 . . . . . . . . 9  |-  F/ y ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. y  e.  A  -.  y  .<_  r )
121 ssel 3347 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
122121ancrd 551 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
( y  e.  B  /\  y  e.  A
) ) )
123122anim1d 561 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
( y  e.  A  /\  -.  y  .<_  r )  ->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) ) )
124123impl 617 . . . . . . . . . . . . 13  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  (
( y  e.  B  /\  y  e.  A
)  /\  -.  y  .<_  r ) )
125 elin 3536 . . . . . . . . . . . . . 14  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( y  e. 
{ z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A
) )
12673elrab 3114 . . . . . . . . . . . . . . 15  |-  ( y  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( y  e.  B  /\  -.  y  .<_  r ) )
127126anbi1i 690 . . . . . . . . . . . . . 14  |-  ( ( y  e.  { z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A )  <->  ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
) )
128 an32 791 . . . . . . . . . . . . . 14  |-  ( ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
)  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
129125, 127, 1283bitri 271 . . . . . . . . . . . . 13  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) )
130124, 129sylibr 212 . . . . . . . . . . . 12  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A
) )
131 ne0i 3640 . . . . . . . . . . . 12  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  ->  ( {
z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
132130, 131syl 16 . . . . . . . . . . 11  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
13326, 132sylanl1 645 . . . . . . . . . 10  |-  ( ( ( ( ( ( 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 )  =/=  (/) )
134133adantllr 713 . . . . . . . . 9  |-  ( ( ( ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. y  e.  A  -.  y  .<_  r )  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
135 simpr 458 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. y  e.  A  -.  y  .<_  r )  ->  E. y  e.  A  -.  y  .<_  r )
136120, 134, 135r19.29af 2859 . . . . . . . 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 )  =/=  (/) )
13792, 117, 136syl2anc 656 . . . . . . 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 )  =/=  (/) )
13818, 11trleile 26044 . . . . . . . . . . . . . . . 16  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  (
r  .<_  z  \/  z  .<_  r ) )
139 oran 493 . . . . . . . . . . . . . . . 16  |-  ( ( r  .<_  z  \/  z  .<_  r )  <->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
140138, 139sylib 196 . . . . . . . . . . . . . . 15  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
1411403expa 1182 . . . . . . . . . . . . . 14  |-  ( ( ( K  e. Toset  /\  r  e.  B )  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
142141nrexdv 2817 . . . . . . . . . . . . 13  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  -.  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
143 rabid 2895 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( z  e.  B  /\  -.  r  .<_  z ) )
144 rabid 2895 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( z  e.  B  /\  -.  z  .<_  r ) )
145143, 144anbi12i 692 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  { z  e.  B  |  -.  r  .<_  z }  /\  z  e.  { z  e.  B  |  -.  z  .<_  r } )  <-> 
( ( z  e.  B  /\  -.  r  .<_  z )  /\  (
z  e.  B  /\  -.  z  .<_  r ) ) )
146 elin 3536 . . . . . . . . . . . . . . . . . 18  |-  ( 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 } ) )
147 anandi 819 . . . . . . . . . . . . . . . . . 18  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  /\  ( z  e.  B  /\  -.  z  .<_  r ) ) )
148145, 146, 1473bitr4i 277 . . . . . . . . . . . . . . . . 17  |-  ( z  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  <->  ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
149148exbii 1639 . . . . . . . . . . . . . . . 16  |-  ( 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 ) ) )
150 nfrab1 2899 . . . . . . . . . . . . . . . . . 18  |-  F/_ z { z  e.  B  |  -.  r  .<_  z }
151 nfrab1 2899 . . . . . . . . . . . . . . . . . 18  |-  F/_ z { z  e.  B  |  -.  z  .<_  r }
152150, 151nfin 3554 . . . . . . . . . . . . . . . . 17  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )
153152n0f 3642 . . . . . . . . . . . . . . . 16  |-  ( ( { 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 } ) )
154 df-rex 2719 . . . . . . . . . . . . . . . 16  |-  ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  E. z ( z  e.  B  /\  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
155149, 153, 1543bitr4ri 278 . . . . . . . . . . . . . . 15  |-  ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <-> 
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )  =/=  (/) )
156 bicom 200 . . . . . . . . . . . . . . 15  |-  ( ( E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) )  <->  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) ) )
157155, 156mpbi 208 . . . . . . . . . . . . . 14  |-  ( ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =/=  (/) 
<->  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
158157necon1bbii 2661 . . . . . . . . . . . . 13  |-  ( -. 
E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r )  <->  ( {
z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
159142, 158sylib 196 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
16028, 159sylancom 662 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
161160adantr 462 . . . . . . . . . 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 } )  =  (/) )
162161ineq1d 3548 . . . . . . . . 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
) )
163 incom 3540 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (
(/)  i^i  A )
164 in0 3660 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (/)
165163, 164eqtr3i 2463 . . . . . . . . 9  |-  ( (/)  i^i 
A )  =  (/)
166162, 165syl6eq 2489 . . . . . . . 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 )  =  (/) )
167166adantlr 709 . . . . . . 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 )  =  (/) )
168 simplr 749 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  r  e.  B )
169 simpr 458 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  -.  r  e.  A )
170 vex 2973 . . . . . . . . . . . . . . 15  |-  r  e. 
_V
171170snss 3996 . . . . . . . . . . . . . 14  |-  ( r  e.  B  <->  { r }  C_  B )
172 eldif 3335 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  ( r  e.  B  /\  -.  r  e.  A ) )
173170snss 3996 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  { r }  C_  ( B  \  A ) )
174172, 173bitr3i 251 . . . . . . . . . . . . . . 15  |-  ( ( r  e.  B  /\  -.  r  e.  A
)  <->  { r }  C_  ( B  \  A ) )
175 ssconb 3486 . . . . . . . . . . . . . . 15  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( {
r }  C_  ( B  \  A )  <->  A  C_  ( B  \  { r } ) ) )
176174, 175syl5bb 257 . . . . . . . . . . . . . 14  |-  ( ( { r }  C_  B  /\  A  C_  B
)  ->  ( (
r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
177171, 176sylanb 469 . . . . . . . . . . . . 13  |-  ( ( r  e.  B  /\  A  C_  B )  -> 
( ( r  e.  B  /\  -.  r  e.  A )  <->  A  C_  ( B  \  { r } ) ) )
178177adantl 463 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  (
r  e.  B  /\  A  C_  B ) )  ->  ( ( r  e.  B  /\  -.  r  e.  A )  <->  A 
C_  ( B  \  { r } ) ) )
179178anass1rs 800 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
180179adantr 462 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
181168, 169, 180mpbi2and 907 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( B  \  {
r } ) )
1828ad3antrrr 724 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  K  e.  Poset )
183 nfv 1678 . . . . . . . . . . 11  |-  F/ z ( K  e.  Poset  /\  r  e.  B )
184150, 151nfun 3509 . . . . . . . . . . 11  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } )
185 nfcv 2577 . . . . . . . . . . 11  |-  F/_ z
( B  \  {
r } )
186 ianor 485 . . . . . . . . . . . . . . 15  |-  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )
18718, 11posrasymb 26035 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  r  =  z ) )
188 equcom 1737 . . . . . . . . . . . . . . . . 17  |-  ( r  =  z  <->  z  =  r )
189187, 188syl6bb 261 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  z  =  r ) )
190189necon3bbid 2640 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  z  =/=  r ) )
191186, 190syl5bbr 259 . . . . . . . . . . . . . 14  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) )
1921913expia 1184 . . . . . . . . . . . . 13  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  B  -> 
( ( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) ) )
193192pm5.32d 634 . . . . . . . . . . . 12  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( z  e.  B  /\  z  =/=  r ) ) )
194143, 144orbi12i 518 . . . . . . . . . . . . 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 ) ) )
195 elun 3494 . . . . . . . . . . . . 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 } ) )
196 andi 857 . . . . . . . . . . . . 13  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( (
z  e.  B  /\  -.  r  .<_  z )  \/  ( z  e.  B  /\  -.  z  .<_  r ) ) )
197194, 195, 1963bitr4ri 278 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  z  e.  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } ) )
198 eldifsn 3997 . . . . . . . . . . . . 13  |-  ( z  e.  ( B  \  { r } )  <-> 
( z  e.  B  /\  z  =/=  r
) )
199198bicomi 202 . . . . . . . . . . . 12  |-  ( ( z  e.  B  /\  z  =/=  r )  <->  z  e.  ( B  \  { r } ) )
200193, 197, 1993bitr3g 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 } ) ) )
201183, 184, 185, 200eqrd 3371 . . . . . . . . . 10  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
202182, 168, 201syl2anc 656 . . . . . . . . 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 } ) )
203181, 202sseqtr4d 3390 . . . . . . . 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 } ) )
204203adantlr 709 . . . . . . 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 } ) )
20525, 27, 70, 89, 116, 137, 167, 204nconsubb 18927 . . . . . 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 )
206205anasss 642 . . . . 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 )
207206adantllr 713 . . . 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 )
208 annim 425 . . . . . . . . . . . . 13  |-  ( ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
209208rexbii 2738 . . . . . . . . . . . 12  |-  ( E. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  E. r  e.  B  -.  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
) )
210 rexnal 2724 . . . . . . . . . . . 12  |-  ( E. r  e.  B  -.  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)  <->  -.  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
211209, 210bitri 249 . . . . . . . . . . 11  |-  ( E. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
212211rexbii 2738 . . . . . . . . . 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
) )
213 rexcom 2880 . . . . . . . . . 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 ) )
214 rexnal 2724 . . . . . . . . . 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
) )
215212, 213, 2143bitr3i 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 ) )
216215rexbii 2738 . . . . . . . 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
) )
217 rexcom 2880 . . . . . . . 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 ) )
218 rexnal 2724 . . . . . . . 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
) )
219216, 217, 2183bitr3i 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 ) )
220 r19.41v 2871 . . . . . . . . . 10  |-  ( E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
221220rexbii 2738 . . . . . . . . 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
) )
222 r19.41v 2871 . . . . . . . . 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 )
)
223 reeanv 2886 . . . . . . . . . 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 ) )
224223anbi1i 690 . . . . . . . . 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 ) )
225221, 222, 2243bitri 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 ) )
226225rexbii 2738 . . . . . . 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 ) )
227219, 226bitr3i 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 ) )
22828ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e. Toset )
22926sselda 3353 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  B )
230168adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  r  e.  B )
23118, 11trleile 26044 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  x  e.  B  /\  r  e.  B )  ->  (
x  .<_  r  \/  r  .<_  x ) )
232228, 229, 230, 231syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  \/  r  .<_  x ) )
233 simpr 458 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  A )
234 simplr 749 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  r  e.  A )
235 nelne2 2700 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  -.  r  e.  A
)  ->  x  =/=  r )
236233, 234, 235syl2anc 656 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  =/=  r )
237182adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e.  Poset
)
23818, 11posrasymb 26035 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  (
( x  .<_  r  /\  r  .<_  x )  <->  x  =  r ) )
239238necon3bbid 2640 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
240237, 229, 230, 239syl3anc 1213 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
241236, 240mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  (
x  .<_  r  /\  r  .<_  x ) )
242232, 241jca 529 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( (
x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) ) )
243 pm5.17 878 . . . . . . . . . . . 12  |-  ( ( ( x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) )  <->  ( x  .<_  r  <->  -.  r  .<_  x ) )
244242, 243sylib 196 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  <->  -.  r  .<_  x ) )
24595, 244rexbida 2728 . . . . . . . . . 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 ) )
24628ad2antrr 720 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e. Toset )
247168adantr 462 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  e.  B )
24826sselda 3353 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  B )
24918, 11trleile 26044 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  r  e.  B  /\  y  e.  B )  ->  (
r  .<_  y  \/  y  .<_  r ) )
250246, 247, 248, 249syl3anc 1213 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  \/  y  .<_  r ) )
251 simpr 458 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  A )
252 simplr 749 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  r  e.  A )
253 nelne2 2700 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  r  e.  A
)  ->  y  =/=  r )
254251, 252, 253syl2anc 656 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  =/=  r )
255254necomd 2693 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  =/=  y )
256182adantr 462 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e.  Poset
)
25718, 11posrasymb 26035 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  (
( r  .<_  y  /\  y  .<_  r )  <->  r  =  y ) )
258257necon3bbid 2640 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
259256, 247, 248, 258syl3anc 1213 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
260255, 259mpbird 232 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  (
r  .<_  y  /\  y  .<_  r ) )
261250, 260jca 529 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( (
r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) ) )
262 pm5.17 878 . . . . . . . . . . . 12  |-  ( ( ( r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) )  <->  ( r  .<_  y 
<->  -.  y  .<_  r ) )
263261, 262sylib 196 . . . . . . . . . . 11  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  <->  -.  y  .<_  r ) )
264118, 263rexbida 2728 . . . . . . . . . 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 ) )
265245, 264anbi12d 705 . . . . . . . . 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 ) ) )
266265ex 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 ) ) ) )
267266pm5.32rd 635 . . . . . . 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
) ) )
2681, 267rexbida 2728 . . . . . 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
) ) )
269227, 268syl5bb 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 )
) )
270269biimpa 481 . . . 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
) )
2717, 207, 270r19.29af 2859 . . 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 )
272271ex 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 ) )
273272con4d 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 960    = wceq 1364   E.wex 1591    e. wcel 1761    =/= wne 2604   A.wral 2713   E.wrex 2714   {crab 2717   _Vcvv 2970    \ cdif 3322    u. cun 3323    i^i cin 3324    C_ wss 3325   (/)c0 3634   {csn 3874   class class class wbr 4289    e. cmpt 4347    X. cxp 4834   dom cdm 4836   ran crn 4837   ` cfv 5415  (class class class)co 6090   ficfi 7656   Basecbs 14170   lecple 14241   ↾t crest 14355   topGenctg 14372  ordTopcordt 14433    Preset cpreset 15092   Posetcpo 15106  Tosetctos 15199  TopOnctopon 18399   Conccon 18915
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-8 1763  ax-9 1765  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422  ax-rep 4400  ax-sep 4410  ax-nul 4418  ax-pow 4467  ax-pr 4528  ax-un 6371
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 961  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-eu 2263  df-mo 2264  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-ne 2606  df-ral 2718  df-rex 2719  df-reu 2720  df-rab 2722  df-v 2972  df-sbc 3184  df-csb 3286  df-dif 3328  df-un 3330  df-in 3332  df-ss 3339  df-pss 3341  df-nul 3635  df-if 3789  df-pw 3859  df-sn 3875  df-pr 3877  df-tp 3879  df-op 3881  df-uni 4089  df-int 4126  df-iun 4170  df-br 4290  df-opab 4348  df-mpt 4349  df-tr 4383  df-eprel 4628  df-id 4632  df-po 4637  df-so 4638  df-fr 4675  df-we 4677  df-ord 4718  df-on 4719  df-lim 4720  df-suc 4721  df-xp 4842  df-rel 4843  df-cnv 4844  df-co 4845  df-dm 4846  df-rn 4847  df-res 4848  df-ima 4849  df-iota 5378  df-fun 5417  df-fn 5418  df-f 5419  df-f1 5420  df-fo 5421  df-f1o 5422  df-fv 5423  df-ov 6093  df-oprab 6094  df-mpt2 6095  df-om 6476  df-1st 6576  df-2nd 6577  df-recs 6828  df-rdg 6862  df-1o 6916  df-oadd 6920  df-er 7097  df-en 7307  df-fin 7310  df-fi 7657  df-rest 14357  df-topgen 14378  df-ordt 14435  df-preset 15094  df-poset 15112  df-toset 15200  df-top 18403  df-bases 18405  df-topon 18406  df-cld 18523  df-con 18916
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator