Metamath Proof Explorer

Theorem axcontlem3

Description: Lemma for axcont . Given the separation assumption, B is a subset of D . (Contributed by Scott Fenton, 18-Jun-2013)

Ref Expression
Hypothesis axcontlem3.1 
|- D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
Assertion axcontlem3 
|- ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> B C_ D )

Proof

Step Hyp Ref Expression
1 axcontlem3.1 
 |-  D = { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) }
2 simplr2 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> B C_ ( EE ` N ) )
3 simpr2 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> U e. A )
4 3 anim1i 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. B ) -> ( U e. A /\ p e. B ) )
5 simplr3 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> A. x e. A A. y e. B x Btwn <. Z , y >. )
6 5 adantr 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. B ) -> A. x e. A A. y e. B x Btwn <. Z , y >. )
7 breq1 
 |-  ( x = U -> ( x Btwn <. Z , y >. <-> U Btwn <. Z , y >. ) )
8 opeq2 
 |-  ( y = p -> <. Z , y >. = <. Z , p >. )
9 8 breq2d 
 |-  ( y = p -> ( U Btwn <. Z , y >. <-> U Btwn <. Z , p >. ) )
10 7 9 rspc2v 
 |-  ( ( U e. A /\ p e. B ) -> ( A. x e. A A. y e. B x Btwn <. Z , y >. -> U Btwn <. Z , p >. ) )
11 4 6 10 sylc 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. B ) -> U Btwn <. Z , p >. )
12 11 orcd 
 |-  ( ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) /\ p e. B ) -> ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) )
13 12 ralrimiva 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> A. p e. B ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) )
14 1 sseq2i 
 |-  ( B C_ D <-> B C_ { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) } )
15 ssrab 
 |-  ( B C_ { p e. ( EE ` N ) | ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) } <-> ( B C_ ( EE ` N ) /\ A. p e. B ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
16 14 15 bitri 
 |-  ( B C_ D <-> ( B C_ ( EE ` N ) /\ A. p e. B ( U Btwn <. Z , p >. \/ p Btwn <. Z , U >. ) ) )
17 2 13 16 sylanbrc 
 |-  ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. Z , y >. ) ) /\ ( Z e. ( EE ` N ) /\ U e. A /\ Z =/= U ) ) -> B C_ D )