Metamath Proof Explorer


Theorem axtgcont1

Description: Axiom of Continuity. Axiom A11 of Schwabhauser p. 13. This axiom (scheme) asserts that any two sets S and T (of points) such that the elements of S precede the elements of T with respect to some point a (that is, x is between a and y whenever x is in X and y is in Y ) are separated by some point b ; this is explained in Axiom 11 of Tarski1999 p. 185. (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 ( 𝜑𝑇𝑃 )
Assertion axtgcont1 ( 𝜑 → ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )

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 df-trkg TarskiG = ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) )
8 inss1 ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ ( TarskiGC ∩ TarskiGB )
9 inss2 ( TarskiGC ∩ TarskiGB ) ⊆ TarskiGB
10 8 9 sstri ( ( TarskiGC ∩ TarskiGB ) ∩ ( TarskiGCB ∩ { 𝑓[ ( Base ‘ 𝑓 ) / 𝑝 ] [ ( Itv ‘ 𝑓 ) / 𝑖 ] ( LineG ‘ 𝑓 ) = ( 𝑥𝑝 , 𝑦 ∈ ( 𝑝 ∖ { 𝑥 } ) ↦ { 𝑧𝑝 ∣ ( 𝑧 ∈ ( 𝑥 𝑖 𝑦 ) ∨ 𝑥 ∈ ( 𝑧 𝑖 𝑦 ) ∨ 𝑦 ∈ ( 𝑥 𝑖 𝑧 ) ) } ) } ) ) ⊆ TarskiGB
11 7 10 eqsstri TarskiG ⊆ TarskiGB
12 11 4 sselid ( 𝜑𝐺 ∈ TarskiGB )
13 1 2 3 istrkgb ( 𝐺 ∈ TarskiGB ↔ ( 𝐺 ∈ V ∧ ( ∀ 𝑥𝑃𝑦𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) ) )
14 13 simprbi ( 𝐺 ∈ TarskiGB → ( ∀ 𝑥𝑃𝑦𝑃 ( 𝑦 ∈ ( 𝑥 𝐼 𝑥 ) → 𝑥 = 𝑦 ) ∧ ∀ 𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ( ( 𝑢 ∈ ( 𝑥 𝐼 𝑧 ) ∧ 𝑣 ∈ ( 𝑦 𝐼 𝑧 ) ) → ∃ 𝑎𝑃 ( 𝑎 ∈ ( 𝑢 𝐼 𝑦 ) ∧ 𝑎 ∈ ( 𝑣 𝐼 𝑥 ) ) ) ∧ ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
15 14 simp3d ( 𝐺 ∈ TarskiGB → ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
16 12 15 syl ( 𝜑 → ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
17 1 fvexi 𝑃 ∈ V
18 17 ssex ( 𝑆𝑃𝑆 ∈ V )
19 elpwg ( 𝑆 ∈ V → ( 𝑆 ∈ 𝒫 𝑃𝑆𝑃 ) )
20 5 18 19 3syl ( 𝜑 → ( 𝑆 ∈ 𝒫 𝑃𝑆𝑃 ) )
21 5 20 mpbird ( 𝜑𝑆 ∈ 𝒫 𝑃 )
22 17 ssex ( 𝑇𝑃𝑇 ∈ V )
23 elpwg ( 𝑇 ∈ V → ( 𝑇 ∈ 𝒫 𝑃𝑇𝑃 ) )
24 6 22 23 3syl ( 𝜑 → ( 𝑇 ∈ 𝒫 𝑃𝑇𝑃 ) )
25 6 24 mpbird ( 𝜑𝑇 ∈ 𝒫 𝑃 )
26 raleq ( 𝑠 = 𝑆 → ( ∀ 𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑥𝑆𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
27 26 rexbidv ( 𝑠 = 𝑆 → ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∃ 𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
28 raleq ( 𝑠 = 𝑆 → ( ∀ 𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∀ 𝑥𝑆𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
29 28 rexbidv ( 𝑠 = 𝑆 → ( ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
30 27 29 imbi12d ( 𝑠 = 𝑆 → ( ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
31 raleq ( 𝑡 = 𝑇 → ( ∀ 𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∀ 𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
32 31 rexralbidv ( 𝑡 = 𝑇 → ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ↔ ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) ) )
33 raleq ( 𝑡 = 𝑇 → ( ∀ 𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∀ 𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
34 33 rexralbidv ( 𝑡 = 𝑇 → ( ∃ 𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ↔ ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )
35 32 34 imbi12d ( 𝑡 = 𝑇 → ( ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ↔ ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
36 30 35 rspc2v ( ( 𝑆 ∈ 𝒫 𝑃𝑇 ∈ 𝒫 𝑃 ) → ( ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) → ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
37 21 25 36 syl2anc ( 𝜑 → ( ∀ 𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃 ( ∃ 𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) → ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) ) )
38 16 37 mpd ( 𝜑 → ( ∃ 𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ ( 𝑎 𝐼 𝑦 ) → ∃ 𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ ( 𝑥 𝐼 𝑦 ) ) )