Metamath Proof Explorer


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 φ G 𝒢 Tarski
axtgcont.1 φ S P
axtgcont.2 φ T P
axtgcont.3 φ A P
axtgcont.4 φ u S v T u A I v
Assertion axtgcont φ b P x S y T b 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 φ G 𝒢 Tarski
5 axtgcont.1 φ S P
6 axtgcont.2 φ T P
7 axtgcont.3 φ A P
8 axtgcont.4 φ u S v T u A I v
9 8 3expb φ u S v T u A I v
10 9 ralrimivva φ u S v T u 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 a I y u A I v
16 15 cbvraldva a = A x = u y T x a I y v T u A I v
17 16 cbvraldva a = A x S y T x a I y u S v T u A I v
18 17 rspcev A P u S v T u A I v a P x S y T x a I y
19 7 10 18 syl2anc φ a P x S y T x a I y
20 1 2 3 4 5 6 axtgcont1 φ a P x S y T x a I y b P x S y T b x I y
21 19 20 mpd φ b P x S y T b x I y