Theorem axcont

Description: The axiom of continuity. Take two sets of points A and B . If all the points in A come before the points of B on a line, then there is a point separating the two. Axiom A11 of Schwabhauser p. 13. (Contributed by Scott Fenton, 20-Jun-2013)

	Ref	Expression
Assertion	axcont	|- ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ E. a e. ( EE ` N ) A. x e. A A. y e. B x Btwn <. a , y >. ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )

Proof

Step	Hyp	Ref	Expression
1		simpr	|- ( ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) -> A. x e. A A. y e. B x Btwn <. a , y >. )
2	1	3anim3i	|- ( ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) -> ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) )
3	2	anim2i	|- ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) ) -> ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) )
4		simpr3l	|- ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) ) -> a e. ( EE ` N ) )
5		axcontlem12	|- ( ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) /\ a e. ( EE ` N ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
6	3 4 5	syl2anc	|- ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )
7	6	3exp2	|- ( N e. NN -> ( A C_ ( EE ` N ) -> ( B C_ ( EE ` N ) -> ( ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) ) )
8	7	com4r	|- ( ( a e. ( EE ` N ) /\ A. x e. A A. y e. B x Btwn <. a , y >. ) -> ( N e. NN -> ( A C_ ( EE ` N ) -> ( B C_ ( EE ` N ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) ) )
9	8	rexlimiva	|- ( E. a e. ( EE ` N ) A. x e. A A. y e. B x Btwn <. a , y >. -> ( N e. NN -> ( A C_ ( EE ` N ) -> ( B C_ ( EE ` N ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) ) )
10	9	com4l	|- ( N e. NN -> ( A C_ ( EE ` N ) -> ( B C_ ( EE ` N ) -> ( E. a e. ( EE ` N ) A. x e. A A. y e. B x Btwn <. a , y >. -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. ) ) ) )
11	10	3imp2	|- ( ( N e. NN /\ ( A C_ ( EE ` N ) /\ B C_ ( EE ` N ) /\ E. a e. ( EE ` N ) A. x e. A A. y e. B x Btwn <. a , y >. ) ) -> E. b e. ( EE ` N ) A. x e. A A. y e. B b Btwn <. x , y >. )