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	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtgcont.1	$⊢ φ \to S \subseteq P$
	axtgcont.2	$⊢ φ \to T \subseteq P$
	axtgcont.3	$⊢ φ \to A \in P$
	axtgcont.4	$⊢ (φ \land u \in S \land v \in T) \to u \in (A I v)$
Assertion	axtgcont	$⊢ φ \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y)$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtgcont.1	$⊢ φ \to S \subseteq P$
6		axtgcont.2	$⊢ φ \to T \subseteq P$
7		axtgcont.3	$⊢ φ \to A \in P$
8		axtgcont.4	$⊢ (φ \land u \in S \land v \in T) \to u \in (A I v)$
9	8	3expb	$⊢ (φ \land (u \in S \land v \in T)) \to u \in (A I v)$
10	9	ralrimivva	$⊢ φ \to \forall u \in S \forall v \in T u \in (A I v)$
11		simplr	$⊢ ((a = A \land x = u) \land y = v) \to x = u$
12		simpll	$⊢ ((a = A \land x = u) \land y = v) \to a = A$
13		simpr	$⊢ ((a = A \land x = u) \land y = v) \to y = v$
14	12 13	oveq12d	$⊢ ((a = A \land x = u) \land y = v) \to a I y = A I v$
15	11 14	eleq12d	$⊢ ((a = A \land x = u) \land y = v) \to (x \in (a I y) \leftrightarrow u \in (A I v))$
16	15	cbvraldva	$⊢ (a = A \land x = u) \to (\forall y \in T x \in (a I y) \leftrightarrow \forall v \in T u \in (A I v))$
17	16	cbvraldva	$⊢ a = A \to (\forall x \in S \forall y \in T x \in (a I y) \leftrightarrow \forall u \in S \forall v \in T u \in (A I v))$
18	17	rspcev	$⊢ (A \in P \land \forall u \in S \forall v \in T u \in (A I v)) \to \exists a \in P \forall x \in S \forall y \in T x \in (a I y)$
19	7 10 18	syl2anc	$⊢ φ \to \exists a \in P \forall x \in S \forall y \in T x \in (a I y)$
20	1 2 3 4 5 6	axtgcont1	$⊢ φ \to (\exists a \in P \forall x \in S \forall y \in T x \in (a I y) \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y))$
21	19 20	mpd	$⊢ φ \to \exists b \in P \forall x \in S \forall y \in T b \in (x I y)$

Metamath Proof Explorer

Theorem axtgcont

Proof