MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  axtgcont1 Structured version   Visualization version   GIF version

Theorem axtgcont1 28271
Description: Axiom of Continuity. Axiom A11 of [Schwabhauser] p. 13. This axiom (scheme) asserts that any two sets 𝑆 and 𝑇 (of points) such that the elements of 𝑆 precede the elements of 𝑇 with respect to some point 𝑎 (that is, 𝑥 is between 𝑎 and 𝑦 whenever 𝑥 is in 𝑋 and 𝑦 is in 𝑌) are separated by some point 𝑏; this is explained in Axiom 11 of [Tarski1999] p. 185. (Contributed by Thierry Arnoux, 16-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p 𝑃 = (Base‘𝐺)
axtrkg.d = (dist‘𝐺)
axtrkg.i 𝐼 = (Itv‘𝐺)
axtrkg.g (𝜑𝐺 ∈ TarskiG)
axtgcont.1 (𝜑𝑆𝑃)
axtgcont.2 (𝜑𝑇𝑃)
Assertion
Ref Expression
axtgcont1 (𝜑 → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
Distinct variable groups:   𝑥,𝑦   𝑎,𝑏,𝑥,𝑦,𝐼   𝑃,𝑎,𝑏,𝑥,𝑦   𝑆,𝑎,𝑏,𝑥   𝑇,𝑎,𝑏,𝑥,𝑦   ,𝑎,𝑏,𝑥,𝑦
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑎,𝑏)   𝑆(𝑦)   𝐺(𝑥,𝑦,𝑎,𝑏)

Proof of Theorem axtgcont1
Dummy variables 𝑓 𝑖 𝑝 𝑧 𝑣 𝑠 𝑡 𝑢 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 28256 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 4229 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss2 4230 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGB
42, 3sstri 3989 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGB
51, 4eqsstri 4014 . . . 4 TarskiG ⊆ TarskiGB
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sselid 3978 . . 3 (𝜑𝐺 ∈ TarskiGB)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgb 28258 . . . . 5 (𝐺 ∈ TarskiGB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))))
1211simprbi 496 . . . 4 (𝐺 ∈ TarskiGB → (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦))))
1312simp3d 1142 . . 3 (𝐺 ∈ TarskiGB → ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
147, 13syl 17 . 2 (𝜑 → ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
15 axtgcont.1 . . . 4 (𝜑𝑆𝑃)
168fvexi 6911 . . . . . 6 𝑃 ∈ V
1716ssex 5321 . . . . 5 (𝑆𝑃𝑆 ∈ V)
18 elpwg 4606 . . . . 5 (𝑆 ∈ V → (𝑆 ∈ 𝒫 𝑃𝑆𝑃))
1915, 17, 183syl 18 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑃𝑆𝑃))
2015, 19mpbird 257 . . 3 (𝜑𝑆 ∈ 𝒫 𝑃)
21 axtgcont.2 . . . 4 (𝜑𝑇𝑃)
2216ssex 5321 . . . . 5 (𝑇𝑃𝑇 ∈ V)
23 elpwg 4606 . . . . 5 (𝑇 ∈ V → (𝑇 ∈ 𝒫 𝑃𝑇𝑃))
2421, 22, 233syl 18 . . . 4 (𝜑 → (𝑇 ∈ 𝒫 𝑃𝑇𝑃))
2521, 24mpbird 257 . . 3 (𝜑𝑇 ∈ 𝒫 𝑃)
26 raleq 3319 . . . . . 6 (𝑠 = 𝑆 → (∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∀𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦)))
2726rexbidv 3175 . . . . 5 (𝑠 = 𝑆 → (∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦)))
28 raleq 3319 . . . . . 6 (𝑠 = 𝑆 → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∀𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
2928rexbidv 3175 . . . . 5 (𝑠 = 𝑆 → (∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
3027, 29imbi12d 344 . . . 4 (𝑠 = 𝑆 → ((∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) ↔ (∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦))))
31 raleq 3319 . . . . . 6 (𝑡 = 𝑇 → (∀𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∀𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦)))
3231rexralbidv 3217 . . . . 5 (𝑡 = 𝑇 → (∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦)))
33 raleq 3319 . . . . . 6 (𝑡 = 𝑇 → (∀𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∀𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
3433rexralbidv 3217 . . . . 5 (𝑡 = 𝑇 → (∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
3532, 34imbi12d 344 . . . 4 (𝑡 = 𝑇 → ((∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) ↔ (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3630, 35rspc2v 3620 . . 3 ((𝑆 ∈ 𝒫 𝑃𝑇 ∈ 𝒫 𝑃) → (∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3720, 25, 36syl2anc 583 . 2 (𝜑 → (∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3814, 37mpd 15 1 (𝜑 → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 395  w3o 1084  w3a 1085   = wceq 1534  wcel 2099  {cab 2705  wral 3058  wrex 3067  {crab 3429  Vcvv 3471  [wsbc 3776  cdif 3944  cin 3946  wss 3947  𝒫 cpw 4603  {csn 4629  cfv 6548  (class class class)co 7420  cmpo 7422  Basecbs 17179  distcds 17241  TarskiGcstrkg 28230  TarskiGCcstrkgc 28231  TarskiGBcstrkgb 28232  TarskiGCBcstrkgcb 28233  Itvcitv 28236  LineGclng 28237
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1790  ax-4 1804  ax-5 1906  ax-6 1964  ax-7 2004  ax-8 2101  ax-9 2109  ax-ext 2699  ax-sep 5299  ax-nul 5306
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 847  df-3an 1087  df-tru 1537  df-fal 1547  df-ex 1775  df-sb 2061  df-clab 2706  df-cleq 2720  df-clel 2806  df-ne 2938  df-ral 3059  df-rex 3068  df-rab 3430  df-v 3473  df-sbc 3777  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4324  df-if 4530  df-pw 4605  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4909  df-br 5149  df-iota 6500  df-fv 6556  df-ov 7423  df-trkgb 28252  df-trkg 28256
This theorem is referenced by:  axtgcont  28272
  Copyright terms: Public domain W3C validator