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 𝑃 = ( 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 ( 𝜑 → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) )