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

Theorem ordtconlem1 26354
Description: Connectedness in the order topology of a toset. This is the "easy" direction of ordtcon 26355. See also reconnlem1 20403. (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 1673 . . . . 5  |-  F/ r ( K  e. Toset  /\  A  C_  B )
2 nfcv 2579 . . . . . . 7  |-  F/_ r A
3 nfra1 2766 . . . . . . . 8  |-  F/ r A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
42, 3nfral 2769 . . . . . . 7  |-  F/ r A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
52, 4nfral 2769 . . . . . 6  |-  F/ r A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x  .<_  r  /\  r  .<_  y )  ->  r  e.  A
)
65nfn 1835 . . . . 5  |-  F/ r  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( ( x 
.<_  r  /\  r  .<_  y )  ->  r  e.  A )
71, 6nfan 1861 . . . 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 26119 . . . . . . . . . 10  |-  ( K  e. Toset  ->  K  e.  Poset )
9 posprs 15119 . . . . . . . . . 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 5701 . . . . . . . . . . . . . . 15  |-  ( le
`  K )  e. 
_V
1312inex1 4433 . . . . . . . . . . . . . 14  |-  ( ( le `  K )  i^i  ( B  X.  B ) )  e. 
_V
1411, 13eqeltri 2513 . . . . . . . . . . . . 13  |-  .<_  e.  _V
15 eqid 2443 . . . . . . . . . . . . . 14  |-  dom  .<_  =  dom  .<_
1615ordttopon 18797 . . . . . . . . . . . . 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 26344 . . . . . . . . . . . . 13  |-  ( K  e.  Preset  ->  dom  .<_  =  B )
2019fveq2d 5695 . . . . . . . . . . . 12  |-  ( K  e.  Preset  ->  (TopOn `  dom  .<_  )  =  (TopOn `  B
) )
2117, 20syl5eleq 2529 . . . . . . . . . . 11  |-  ( K  e.  Preset  ->  (ordTop `  .<_  )  e.  (TopOn `  B )
)
2210, 21syl5eqel 2527 . . . . . . . . . 10  |-  ( K  e.  Preset  ->  J  e.  (TopOn `  B ) )
238, 9, 223syl 20 . . . . . . . . 9  |-  ( K  e. Toset  ->  J  e.  (TopOn `  B ) )
2423ad3antrrr 729 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
2524adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  J  e.  (TopOn `  B )
)
26 simpllr 758 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  B )
2726adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  A  C_  B )
28 simpll 753 . . . . . . . . . . . . 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 4533 . . . . . . . . . . . . . . . . 17  |-  { B }  e.  _V
31 fvex 5701 . . . . . . . . . . . . . . . . . . . . 21  |-  ( Base `  K )  e.  _V
3218, 31eqeltri 2513 . . . . . . . . . . . . . . . . . . . 20  |-  B  e. 
_V
3332mptex 5948 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  e.  _V
3433rnex 6512 . . . . . . . . . . . . . . . . . 18  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  e.  _V
3532mptex 5948 . . . . . . . . . . . . . . . . . . 19  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3635rnex 6512 . . . . . . . . . . . . . . . . . 18  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  e.  _V
3734, 36unex 6378 . . . . . . . . . . . . . . . . 17  |-  ( ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  u.  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } ) )  e.  _V
3830, 37unex 6378 . . . . . . . . . . . . . . . 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 7669 . . . . . . . . . . . . . . . 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 5701 . . . . . . . . . . . . . . . 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 18571 . . . . . . . . . . . . . . . 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 3365 . . . . . . . . . . . . . 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 2443 . . . . . . . . . . . . . . . 16  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)
46 eqid 2443 . . . . . . . . . . . . . . . 16  |-  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ran  (
x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
4718, 11, 45, 46ordtprsval 26348 . . . . . . . . . . . . . . 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 2487 . . . . . . . . . . . . . 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 3405 . . . . . . . . . . . . 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 3534 . . . . . . . . . . . 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 3534 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  C_  J )
53 breq2 4296 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
r  .<_  z  <->  r  .<_  y ) )
5453notbid 294 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  ( -.  r  .<_  z  <->  -.  r  .<_  y ) )
5554cbvrabv 2971 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y }
56 breq1 4295 . . . . . . . . . . . . . . . . 17  |-  ( x  =  r  ->  (
x  .<_  y  <->  r  .<_  y ) )
5756notbid 294 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  ( -.  x  .<_  y  <->  -.  r  .<_  y ) )
5857rabbidv 2964 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  { y  e.  B  |  -.  x  .<_  y }  =  { y  e.  B  |  -.  r  .<_  y } )
5958eqeq2d 2454 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y }  <->  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  r  .<_  y } ) )
6059rspcev 3073 . . . . . . . . . . . . 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 671 . . . . . . . . . . . 12  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  r  .<_  z }  =  { y  e.  B  |  -.  x  .<_  y } )
6232rabex 4443 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  r  .<_  z }  e.  _V
63 eqid 2443 . . . . . . . . . . . . . 14  |-  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  x  .<_  y } )
6463elrnmpt 5086 . . . . . . . . . . . . 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 466 . . . . . . . . . 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 3357 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
6968adantr 465 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
7069adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  r  .<_  z }  e.  J )
7151unssad 3533 . . . . . . . . . 10  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ran  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x }
)  C_  J )
72 breq1 4295 . . . . . . . . . . . . . . 15  |-  ( z  =  y  ->  (
z  .<_  r  <->  y  .<_  r ) )
7372notbid 294 . . . . . . . . . . . . . 14  |-  ( z  =  y  ->  ( -.  z  .<_  r  <->  -.  y  .<_  r ) )
7473cbvrabv 2971 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r }
75 breq2 4296 . . . . . . . . . . . . . . . . 17  |-  ( x  =  r  ->  (
y  .<_  x  <->  y  .<_  r ) )
7675notbid 294 . . . . . . . . . . . . . . . 16  |-  ( x  =  r  ->  ( -.  y  .<_  x  <->  -.  y  .<_  r ) )
7776rabbidv 2964 . . . . . . . . . . . . . . 15  |-  ( x  =  r  ->  { y  e.  B  |  -.  y  .<_  x }  =  { y  e.  B  |  -.  y  .<_  r } )
7877eqeq2d 2454 . . . . . . . . . . . . . 14  |-  ( x  =  r  ->  ( { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }  <->  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  r } ) )
7978rspcev 3073 . . . . . . . . . . . . 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 671 . . . . . . . . . . . 12  |-  ( r  e.  B  ->  E. x  e.  B  { z  e.  B  |  -.  z  .<_  r }  =  { y  e.  B  |  -.  y  .<_  x }
)
8132rabex 4443 . . . . . . . . . . . . 13  |-  { z  e.  B  |  -.  z  .<_  r }  e.  _V
82 eqid 2443 . . . . . . . . . . . . . 14  |-  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )  =  ( x  e.  B  |->  { y  e.  B  |  -.  y  .<_  x } )
8382elrnmpt 5086 . . . . . . . . . . . . 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 466 . . . . . . . . . 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 3357 . . . . . . . . 9  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8887adantr 465 . . . . . . . 8  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
8988adantlr 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  { z  e.  B  |  -.  z  .<_  r }  e.  J )
90 simpll 753 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( K  e. Toset  /\  A  C_  B )  /\  r  e.  B ) )
91 simpr 461 . . . . . . . . 9  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  -.  r  e.  A )
9290, 91jca 532 . . . . . . . 8  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A ) )
93 simplr 754 . . . . . . . . 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 459 . . . . . . . 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 1673 . . . . . . . . . 10  |-  F/ x
( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )
96 nfre1 2772 . . . . . . . . . 10  |-  F/ x E. x  e.  A  -.  r  .<_  x
9795, 96nfan 1861 . . . . . . . . 9  |-  F/ x
( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. x  e.  A  -.  r  .<_  x )
98 ssel 3350 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  B  ->  (
x  e.  A  ->  x  e.  B )
)
9998ancrd 554 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
x  e.  A  -> 
( x  e.  B  /\  x  e.  A
) ) )
10099anim1d 564 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
( x  e.  A  /\  -.  r  .<_  x )  ->  ( ( x  e.  B  /\  x  e.  A )  /\  -.  r  .<_  x ) ) )
101100impl 620 . . . . . . . . . . . . 13  |-  ( ( ( A  C_  B  /\  x  e.  A
)  /\  -.  r  .<_  x )  ->  (
( x  e.  B  /\  x  e.  A
)  /\  -.  r  .<_  x ) )
102 elin 3539 . . . . . . . . . . . . . 14  |-  ( x  e.  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  <->  ( x  e. 
{ z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A
) )
103 breq2 4296 . . . . . . . . . . . . . . . . 17  |-  ( z  =  x  ->  (
r  .<_  z  <->  r  .<_  x ) )
104103notbid 294 . . . . . . . . . . . . . . . 16  |-  ( z  =  x  ->  ( -.  r  .<_  z  <->  -.  r  .<_  x ) )
105104elrab 3117 . . . . . . . . . . . . . . 15  |-  ( x  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( x  e.  B  /\  -.  r  .<_  x ) )
106105anbi1i 695 . . . . . . . . . . . . . 14  |-  ( ( x  e.  { z  e.  B  |  -.  r  .<_  z }  /\  x  e.  A )  <->  ( ( x  e.  B  /\  -.  r  .<_  x )  /\  x  e.  A
) )
107 an32 796 . . . . . . . . . . . . . 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 3643 . . . . . . . . . . . 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 650 . . . . . . . . . 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 718 . . . . . . . . 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 461 . . . . . . . . 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 2861 . . . . . . . 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 661 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  A )  =/=  (/) )
11793simprd 463 . . . . . . . 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 1673 . . . . . . . . . 10  |-  F/ y ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )
119 nfre1 2772 . . . . . . . . . 10  |-  F/ y E. y  e.  A  -.  y  .<_  r
120118, 119nfan 1861 . . . . . . . . 9  |-  F/ y ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  /\  -.  r  e.  A )  /\  E. y  e.  A  -.  y  .<_  r )
121 ssel 3350 . . . . . . . . . . . . . . . 16  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
y  e.  B ) )
122121ancrd 554 . . . . . . . . . . . . . . 15  |-  ( A 
C_  B  ->  (
y  e.  A  -> 
( y  e.  B  /\  y  e.  A
) ) )
123122anim1d 564 . . . . . . . . . . . . . 14  |-  ( A 
C_  B  ->  (
( y  e.  A  /\  -.  y  .<_  r )  ->  ( ( y  e.  B  /\  y  e.  A )  /\  -.  y  .<_  r ) ) )
124123impl 620 . . . . . . . . . . . . 13  |-  ( ( ( A  C_  B  /\  y  e.  A
)  /\  -.  y  .<_  r )  ->  (
( y  e.  B  /\  y  e.  A
)  /\  -.  y  .<_  r ) )
125 elin 3539 . . . . . . . . . . . . . 14  |-  ( y  e.  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  <->  ( y  e. 
{ z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A
) )
12673elrab 3117 . . . . . . . . . . . . . . 15  |-  ( y  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( y  e.  B  /\  -.  y  .<_  r ) )
127126anbi1i 695 . . . . . . . . . . . . . 14  |-  ( ( y  e.  { z  e.  B  |  -.  z  .<_  r }  /\  y  e.  A )  <->  ( ( y  e.  B  /\  -.  y  .<_  r )  /\  y  e.  A
) )
128 an32 796 . . . . . . . . . . . . . 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 3643 . . . . . . . . . . . 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 650 . . . . . . . . . 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 718 . . . . . . . . 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 461 . . . . . . . . 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 2861 . . . . . . . 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 661 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  z  .<_  r }  i^i  A )  =/=  (/) )
13818, 11trleile 26127 . . . . . . . . . . . . . . . 16  |-  ( ( K  e. Toset  /\  r  e.  B  /\  z  e.  B )  ->  (
r  .<_  z  \/  z  .<_  r ) )
139 oran 496 . . . . . . . . . . . . . . . 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 1187 . . . . . . . . . . . . . 14  |-  ( ( ( K  e. Toset  /\  r  e.  B )  /\  z  e.  B )  ->  -.  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
142141nrexdv 2819 . . . . . . . . . . . . 13  |-  ( ( K  e. Toset  /\  r  e.  B )  ->  -.  E. z  e.  B  ( -.  r  .<_  z  /\  -.  z  .<_  r ) )
143 rabid 2897 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { z  e.  B  |  -.  r  .<_  z }  <->  ( z  e.  B  /\  -.  r  .<_  z ) )
144 rabid 2897 . . . . . . . . . . . . . . . . . . 19  |-  ( z  e.  { z  e.  B  |  -.  z  .<_  r }  <->  ( z  e.  B  /\  -.  z  .<_  r ) )
145143, 144anbi12i 697 . . . . . . . . . . . . . . . . . 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 3539 . . . . . . . . . . . . . . . . . 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 824 . . . . . . . . . . . . . . . . . 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 1634 . . . . . . . . . . . . . . . 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 2901 . . . . . . . . . . . . . . . . . 18  |-  F/_ z { z  e.  B  |  -.  r  .<_  z }
151 nfrab1 2901 . . . . . . . . . . . . . . . . . 18  |-  F/_ z { z  e.  B  |  -.  z  .<_  r }
152150, 151nfin 3557 . . . . . . . . . . . . . . . . 17  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )
153152n0f 3645 . . . . . . . . . . . . . . . 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 2721 . . . . . . . . . . . . . . . 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 2663 . . . . . . . . . . . . 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 667 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
161160adantr 465 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  i^i  { z  e.  B  |  -.  z  .<_  r } )  =  (/) )
162161ineq1d 3551 . . . . . . . . 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 3543 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (
(/)  i^i  A )
164 in0 3663 . . . . . . . . . 10  |-  ( A  i^i  (/) )  =  (/)
165163, 164eqtr3i 2465 . . . . . . . . 9  |-  ( (/)  i^i 
A )  =  (/)
166162, 165syl6eq 2491 . . . . . . . 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 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  (
( { z  e.  B  |  -.  r  .<_  z }  i^i  {
z  e.  B  |  -.  z  .<_  r } )  i^i  A )  =  (/) )
168 simplr 754 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  r  e.  B )
169 simpr 461 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  -.  r  e.  A )
170 vex 2975 . . . . . . . . . . . . . . 15  |-  r  e. 
_V
171170snss 3999 . . . . . . . . . . . . . 14  |-  ( r  e.  B  <->  { r }  C_  B )
172 eldif 3338 . . . . . . . . . . . . . . . 16  |-  ( r  e.  ( B  \  A )  <->  ( r  e.  B  /\  -.  r  e.  A ) )
173170snss 3999 . . . . . . . . . . . . . . . 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 3489 . . . . . . . . . . . . . . 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 472 . . . . . . . . . . . . 13  |-  ( ( r  e.  B  /\  A  C_  B )  -> 
( ( r  e.  B  /\  -.  r  e.  A )  <->  A  C_  ( B  \  { r } ) ) )
178177adantl 466 . . . . . . . . . . . 12  |-  ( ( K  e. Toset  /\  (
r  e.  B  /\  A  C_  B ) )  ->  ( ( r  e.  B  /\  -.  r  e.  A )  <->  A 
C_  ( B  \  { r } ) ) )
179178anass1rs 805 . . . . . . . . . . 11  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( r  e.  B  /\  -.  r  e.  A
)  <->  A  C_  ( B 
\  { r } ) ) )
180179adantr 465 . . . . . . . . . 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 912 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  A  C_  ( B  \  {
r } ) )
1828ad3antrrr 729 . . . . . . . . . 10  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  K  e.  Poset )
183 nfv 1673 . . . . . . . . . . 11  |-  F/ z ( K  e.  Poset  /\  r  e.  B )
184150, 151nfun 3512 . . . . . . . . . . 11  |-  F/_ z
( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } )
185 nfcv 2579 . . . . . . . . . . 11  |-  F/_ z
( B  \  {
r } )
186 ianor 488 . . . . . . . . . . . . . . 15  |-  ( -.  ( r  .<_  z  /\  z  .<_  r )  <->  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )
18718, 11posrasymb 26118 . . . . . . . . . . . . . . . . 17  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  z  e.  B )  ->  (
( r  .<_  z  /\  z  .<_  r )  <->  r  =  z ) )
188 equcom 1732 . . . . . . . . . . . . . . . . 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 2642 . . . . . . . . . . . . . . 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 1189 . . . . . . . . . . . . 13  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
z  e.  B  -> 
( ( -.  r  .<_  z  \/  -.  z  .<_  r )  <->  z  =/=  r ) ) )
193192pm5.32d 639 . . . . . . . . . . . 12  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  (
( z  e.  B  /\  ( -.  r  .<_  z  \/  -.  z  .<_  r ) )  <->  ( z  e.  B  /\  z  =/=  r ) ) )
194143, 144orbi12i 521 . . . . . . . . . . . . 13  |-  ( ( z  e.  { z  e.  B  |  -.  r  .<_  z }  \/  z  e.  { z  e.  B  |  -.  z  .<_  r } )  <-> 
( ( z  e.  B  /\  -.  r  .<_  z )  \/  (
z  e.  B  /\  -.  z  .<_  r ) ) )
195 elun 3497 . . . . . . . . . . . . 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 862 . . . . . . . . . . . . 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 4000 . . . . . . . . . . . . 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 3374 . . . . . . . . . 10  |-  ( ( K  e.  Poset  /\  r  e.  B )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
202182, 168, 201syl2anc 661 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  ( { z  e.  B  |  -.  r  .<_  z }  u.  { z  e.  B  |  -.  z  .<_  r } )  =  ( B  \  {
r } ) )
203181, 202sseqtr4d 3393 . . . . . . . 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 714 . . . . . . 7  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) )  /\  -.  r  e.  A )  ->  A  C_  ( { z  e.  B  |  -.  r  .<_  z }  u.  {
z  e.  B  |  -.  z  .<_  r } ) )
20525, 27, 70, 89, 116, 137, 167, 204nconsubb 19027 . . . . . 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 647 . . . . 5  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) )  ->  -.  ( Jt  A )  e.  Con )
207206adantllr 718 . . . 4  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )  /\  r  e.  B )  /\  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A )
)  ->  -.  ( Jt  A )  e.  Con )
208 annim 425 . . . . . . . . . . . . 13  |-  ( ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  -.  ( (
x  .<_  r  /\  r  .<_  y )  ->  r  e.  A ) )
209208rexbii 2740 . . . . . . . . . . . 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 2726 . . . . . . . . . . . 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 2740 . . . . . . . . . 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 2882 . . . . . . . . . 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 2726 . . . . . . . . . 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 2740 . . . . . . . 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 2882 . . . . . . . 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 2726 . . . . . . . 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 2873 . . . . . . . . . 10  |-  ( E. y  e.  A  ( ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A )
)
221220rexbii 2740 . . . . . . . . 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 2873 . . . . . . . . 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 2888 . . . . . . . . . 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 695 . . . . . . . . 9  |-  ( ( E. x  e.  A  E. y  e.  A  ( x  .<_  r  /\  r  .<_  y )  /\  -.  r  e.  A
)  <->  ( ( E. x  e.  A  x 
.<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A ) )
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 2740 . . . . . . 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 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e. Toset )
22926sselda 3356 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  B )
230168adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  r  e.  B )
23118, 11trleile 26127 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  x  e.  B  /\  r  e.  B )  ->  (
x  .<_  r  \/  r  .<_  x ) )
232228, 229, 230, 231syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( x  .<_  r  \/  r  .<_  x ) )
233 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  e.  A )
234 simplr 754 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  -.  r  e.  A )
235 nelne2 2702 . . . . . . . . . . . . . . 15  |-  ( ( x  e.  A  /\  -.  r  e.  A
)  ->  x  =/=  r )
236233, 234, 235syl2anc 661 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  x  =/=  r )
237182adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  K  e.  Poset
)
23818, 11posrasymb 26118 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  (
( x  .<_  r  /\  r  .<_  x )  <->  x  =  r ) )
239238necon3bbid 2642 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  x  e.  B  /\  r  e.  B )  ->  ( -.  ( x  .<_  r  /\  r  .<_  x )  <->  x  =/=  r ) )
240237, 229, 230, 239syl3anc 1218 . . . . . . . . . . . . . 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 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  x  e.  A
)  ->  ( (
x  .<_  r  \/  r  .<_  x )  /\  -.  ( x  .<_  r  /\  r  .<_  x ) ) )
243 pm5.17 883 . . . . . . . . . . . 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 2730 . . . . . . . . . 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 725 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e. Toset )
247168adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  e.  B )
24826sselda 3356 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  B )
24918, 11trleile 26127 . . . . . . . . . . . . . 14  |-  ( ( K  e. Toset  /\  r  e.  B  /\  y  e.  B )  ->  (
r  .<_  y  \/  y  .<_  r ) )
250246, 247, 248, 249syl3anc 1218 . . . . . . . . . . . . 13  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( r  .<_  y  \/  y  .<_  r ) )
251 simpr 461 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  e.  A )
252 simplr 754 . . . . . . . . . . . . . . . 16  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  -.  r  e.  A )
253 nelne2 2702 . . . . . . . . . . . . . . . 16  |-  ( ( y  e.  A  /\  -.  r  e.  A
)  ->  y  =/=  r )
254251, 252, 253syl2anc 661 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  y  =/=  r )
255254necomd 2695 . . . . . . . . . . . . . 14  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  r  =/=  y )
256182adantr 465 . . . . . . . . . . . . . . 15  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  K  e.  Poset
)
25718, 11posrasymb 26118 . . . . . . . . . . . . . . . 16  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  (
( r  .<_  y  /\  y  .<_  r )  <->  r  =  y ) )
258257necon3bbid 2642 . . . . . . . . . . . . . . 15  |-  ( ( K  e.  Poset  /\  r  e.  B  /\  y  e.  B )  ->  ( -.  ( r  .<_  y  /\  y  .<_  r )  <->  r  =/=  y ) )
259256, 247, 248, 258syl3anc 1218 . . . . . . . . . . . . . 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 532 . . . . . . . . . . . 12  |-  ( ( ( ( ( K  e. Toset  /\  A  C_  B
)  /\  r  e.  B )  /\  -.  r  e.  A )  /\  y  e.  A
)  ->  ( (
r  .<_  y  \/  y  .<_  r )  /\  -.  ( r  .<_  y  /\  y  .<_  r ) ) )
262 pm5.17 883 . . . . . . . . . . . 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 2730 . . . . . . . . . 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 710 . . . . . . . . 9  |-  ( ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B
)  /\  -.  r  e.  A )  ->  (
( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r 
.<_  y )  <->  ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r ) ) )
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 640 . . . . . . 7  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  r  e.  B )  ->  (
( ( E. x  e.  A  x  .<_  r  /\  E. y  e.  A  r  .<_  y )  /\  -.  r  e.  A )  <->  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) ) )
2681, 267rexbida 2730 . . . . . 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 484 . . . 4  |-  ( ( ( K  e. Toset  /\  A  C_  B )  /\  -.  A. x  e.  A  A. y  e.  A  A. r  e.  B  (
( x  .<_  r  /\  r  .<_  y )  -> 
r  e.  A ) )  ->  E. r  e.  B  ( ( E. x  e.  A  -.  r  .<_  x  /\  E. y  e.  A  -.  y  .<_  r )  /\  -.  r  e.  A
) )
2717, 207, 270r19.29af 2861 . . 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 965    = wceq 1369   E.wex 1586    e. wcel 1756    =/= wne 2606   A.wral 2715   E.wrex 2716   {crab 2719   _Vcvv 2972    \ cdif 3325    u. cun 3326    i^i cin 3327    C_ wss 3328   (/)c0 3637   {csn 3877   class class class wbr 4292    e. cmpt 4350    X. cxp 4838   dom cdm 4840   ran crn 4841   ` cfv 5418  (class class class)co 6091   ficfi 7660   Basecbs 14174   lecple 14245   ↾t crest 14359   topGenctg 14376  ordTopcordt 14437    Preset cpreset 15096   Posetcpo 15110  Tosetctos 15203  TopOnctopon 18499   Conccon 19015
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423  ax-rep 4403  ax-sep 4413  ax-nul 4421  ax-pow 4470  ax-pr 4531  ax-un 6372
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 966  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2257  df-mo 2258  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2568  df-ne 2608  df-ral 2720  df-rex 2721  df-reu 2722  df-rab 2724  df-v 2974  df-sbc 3187  df-csb 3289  df-dif 3331  df-un 3333  df-in 3335  df-ss 3342  df-pss 3344  df-nul 3638  df-if 3792  df-pw 3862  df-sn 3878  df-pr 3880  df-tp 3882  df-op 3884  df-uni 4092  df-int 4129  df-iun 4173  df-br 4293  df-opab 4351  df-mpt 4352  df-tr 4386  df-eprel 4632  df-id 4636  df-po 4641  df-so 4642  df-fr 4679  df-we 4681  df-ord 4722  df-on 4723  df-lim 4724  df-suc 4725  df-xp 4846  df-rel 4847  df-cnv 4848  df-co 4849  df-dm 4850  df-rn 4851  df-res 4852  df-ima 4853  df-iota 5381  df-fun 5420  df-fn 5421  df-f 5422  df-f1 5423  df-fo 5424  df-f1o 5425  df-fv 5426  df-ov 6094  df-oprab 6095  df-mpt2 6096  df-om 6477  df-1st 6577  df-2nd 6578  df-recs 6832  df-rdg 6866  df-1o 6920  df-oadd 6924  df-er 7101  df-en 7311  df-fin 7314  df-fi 7661  df-rest 14361  df-topgen 14382  df-ordt 14439  df-preset 15098  df-poset 15116  df-toset 15204  df-top 18503  df-bases 18505  df-topon 18506  df-cld 18623  df-con 19016
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator