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	⊢ 𝑃 = ( Base ‘ 𝐺 )
	axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
	axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
	axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
	axtgcont.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑃 )
	axtgcont.2	⊢ ( 𝜑 → 𝑇 ⊆ 𝑃 )
	axtgcont.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
	axtgcont.4	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) → 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) )
Assertion	axtgcont	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) )

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	⊢ 𝑃 = ( Base ‘ 𝐺 )
2		axtrkg.d	⊢ − = ( dist ‘ 𝐺 )
3		axtrkg.i	⊢ 𝐼 = ( Itv ‘ 𝐺 )
4		axtrkg.g	⊢ ( 𝜑 → 𝐺 ∈ TarskiG )
5		axtgcont.1	⊢ ( 𝜑 → 𝑆 ⊆ 𝑃 )
6		axtgcont.2	⊢ ( 𝜑 → 𝑇 ⊆ 𝑃 )
7		axtgcont.3	⊢ ( 𝜑 → 𝐴 ∈ 𝑃 )
8		axtgcont.4	⊢ ( ( 𝜑 ∧ 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) → 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) )
9	8	3expb	⊢ ( ( 𝜑 ∧ ( 𝑢 ∈ 𝑆 ∧ 𝑣 ∈ 𝑇 ) ) → 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) )
10	9	ralrimivva	⊢ ( 𝜑 → ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) )
11		simplr	⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑥 = 𝑢 )
12		simpll	⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑎 = 𝐴 )
13		simpr	⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → 𝑦 = 𝑣 )
14	12 13	oveq12d	⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → ( 𝑎 𝐼 𝑦 ) = ( 𝐴 𝐼 𝑣 ) )
15	11 14	eleq12d	⊢ ( ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) ∧ 𝑦 = 𝑣 ) → ( 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) )
16	15	cbvraldva	⊢ ( ( 𝑎 = 𝐴 ∧ 𝑥 = 𝑢 ) → ( ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) )
17	16	cbvraldva	⊢ ( 𝑎 = 𝐴 → ( ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) )
18	17	rspcev	⊢ ( ( 𝐴 ∈ 𝑃 ∧ ∀ 𝑢 ∈ 𝑆 ∀ 𝑣 ∈ 𝑇 𝑢 ∈ ( 𝐴 𝐼 𝑣 ) ) → ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) )
19	7 10 18	syl2anc	⊢ ( 𝜑 → ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) )
20	1 2 3 4 5 6	axtgcont1	⊢ ( 𝜑 → ( ∃ 𝑎 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
21	19 20	mpd	⊢ ( 𝜑 → ∃ 𝑏 ∈ 𝑃 ∀ 𝑥 ∈ 𝑆 ∀ 𝑦 ∈ 𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) )