Theorem axtgcont

Description: Axiom of Continuity. Axiom A11 of Schwabhauser p. 13. For more information see axtgcont1 . (Contributed by Thierry Arnoux, 16-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	|- P = ( Base ` G )
	axtrkg.d	|- .- = ( dist ` G )
	axtrkg.i	|- I = ( Itv ` G )
	axtrkg.g	|- ( ph -> G e. TarskiG )
	axtgcont.1	|- ( ph -> S C_ P )
	axtgcont.2	|- ( ph -> T C_ P )
	axtgcont.3	|- ( ph -> A e. P )
	axtgcont.4	|- ( ( ph /\ u e. S /\ v e. T ) -> u e. ( A I v ) )
Assertion	axtgcont	|- ( ph -> E. b e. P A. x e. S A. y e. T b e. ( x I y ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	|- P = ( Base ` G )
2		axtrkg.d	|- .- = ( dist ` G )
3		axtrkg.i	|- I = ( Itv ` G )
4		axtrkg.g	|- ( ph -> G e. TarskiG )
5		axtgcont.1	|- ( ph -> S C_ P )
6		axtgcont.2	|- ( ph -> T C_ P )
7		axtgcont.3	|- ( ph -> A e. P )
8		axtgcont.4	|- ( ( ph /\ u e. S /\ v e. T ) -> u e. ( A I v ) )
9	8	3expb	|- ( ( ph /\ ( u e. S /\ v e. T ) ) -> u e. ( A I v ) )
10	9	ralrimivva	|- ( ph -> A. u e. S A. v e. T u e. ( A I v ) )
11		simplr	|- ( ( ( a = A /\ x = u ) /\ y = v ) -> x = u )
12		simpll	|- ( ( ( a = A /\ x = u ) /\ y = v ) -> a = A )
13		simpr	|- ( ( ( a = A /\ x = u ) /\ y = v ) -> y = v )
14	12 13	oveq12d	|- ( ( ( a = A /\ x = u ) /\ y = v ) -> ( a I y ) = ( A I v ) )
15	11 14	eleq12d	|- ( ( ( a = A /\ x = u ) /\ y = v ) -> ( x e. ( a I y ) <-> u e. ( A I v ) ) )
16	15	cbvraldva	|- ( ( a = A /\ x = u ) -> ( A. y e. T x e. ( a I y ) <-> A. v e. T u e. ( A I v ) ) )
17	16	cbvraldva	|- ( a = A -> ( A. x e. S A. y e. T x e. ( a I y ) <-> A. u e. S A. v e. T u e. ( A I v ) ) )
18	17	rspcev	|- ( ( A e. P /\ A. u e. S A. v e. T u e. ( A I v ) ) -> E. a e. P A. x e. S A. y e. T x e. ( a I y ) )
19	7 10 18	syl2anc	|- ( ph -> E. a e. P A. x e. S A. y e. T x e. ( a I y ) )
20	1 2 3 4 5 6	axtgcont1	|- ( ph -> ( E. a e. P A. x e. S A. y e. T x e. ( a I y ) -> E. b e. P A. x e. S A. y e. T b e. ( x I y ) ) )
21	19 20	mpd	|- ( ph -> E. b e. P A. x e. S A. y e. T b e. ( x I y ) )