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

Theorem axtgcont1 27410
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 27395 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 4188 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss2 4189 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGB
42, 3sstri 3953 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGB
51, 4eqsstri 3978 . . . 4 TarskiG ⊆ TarskiGB
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sselid 3942 . . 3 (𝜑𝐺 ∈ TarskiGB)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgb 27397 . . . . 5 (𝐺 ∈ TarskiGB ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))))
1211simprbi 497 . . . 4 (𝐺 ∈ TarskiGB → (∀𝑥𝑃𝑦𝑃 (𝑦 ∈ (𝑥𝐼𝑥) → 𝑥 = 𝑦) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃𝑢𝑃𝑣𝑃 ((𝑢 ∈ (𝑥𝐼𝑧) ∧ 𝑣 ∈ (𝑦𝐼𝑧)) → ∃𝑎𝑃 (𝑎 ∈ (𝑢𝐼𝑦) ∧ 𝑎 ∈ (𝑣𝐼𝑥))) ∧ ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦))))
1312simp3d 1144 . . 3 (𝐺 ∈ TarskiGB → ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
147, 13syl 17 . 2 (𝜑 → ∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
15 axtgcont.1 . . . 4 (𝜑𝑆𝑃)
168fvexi 6856 . . . . . 6 𝑃 ∈ V
1716ssex 5278 . . . . 5 (𝑆𝑃𝑆 ∈ V)
18 elpwg 4563 . . . . 5 (𝑆 ∈ V → (𝑆 ∈ 𝒫 𝑃𝑆𝑃))
1915, 17, 183syl 18 . . . 4 (𝜑 → (𝑆 ∈ 𝒫 𝑃𝑆𝑃))
2015, 19mpbird 256 . . 3 (𝜑𝑆 ∈ 𝒫 𝑃)
21 axtgcont.2 . . . 4 (𝜑𝑇𝑃)
2216ssex 5278 . . . . 5 (𝑇𝑃𝑇 ∈ V)
23 elpwg 4563 . . . . 5 (𝑇 ∈ V → (𝑇 ∈ 𝒫 𝑃𝑇𝑃))
2421, 22, 233syl 18 . . . 4 (𝜑 → (𝑇 ∈ 𝒫 𝑃𝑇𝑃))
2521, 24mpbird 256 . . 3 (𝜑𝑇 ∈ 𝒫 𝑃)
26 raleq 3309 . . . . . 6 (𝑠 = 𝑆 → (∀𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∀𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦)))
2726rexbidv 3175 . . . . 5 (𝑠 = 𝑆 → (∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦)))
28 raleq 3309 . . . . . 6 (𝑠 = 𝑆 → (∀𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∀𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
2928rexbidv 3175 . . . . 5 (𝑠 = 𝑆 → (∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)))
3027, 29imbi12d 344 . . . 4 (𝑠 = 𝑆 → ((∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) ↔ (∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦))))
31 raleq 3309 . . . . . 6 (𝑡 = 𝑇 → (∀𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∀𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦)))
3231rexralbidv 3214 . . . . 5 (𝑡 = 𝑇 → (∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) ↔ ∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦)))
33 raleq 3309 . . . . . 6 (𝑡 = 𝑇 → (∀𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∀𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
3433rexralbidv 3214 . . . . 5 (𝑡 = 𝑇 → (∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦) ↔ ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
3532, 34imbi12d 344 . . . 4 (𝑡 = 𝑇 → ((∃𝑎𝑃𝑥𝑆𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) ↔ (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3630, 35rspc2v 3590 . . 3 ((𝑆 ∈ 𝒫 𝑃𝑇 ∈ 𝒫 𝑃) → (∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3720, 25, 36syl2anc 584 . 2 (𝜑 → (∀𝑠 ∈ 𝒫 𝑃𝑡 ∈ 𝒫 𝑃(∃𝑎𝑃𝑥𝑠𝑦𝑡 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑠𝑦𝑡 𝑏 ∈ (𝑥𝐼𝑦)) → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦))))
3814, 37mpd 15 1 (𝜑 → (∃𝑎𝑃𝑥𝑆𝑦𝑇 𝑥 ∈ (𝑎𝐼𝑦) → ∃𝑏𝑃𝑥𝑆𝑦𝑇 𝑏 ∈ (𝑥𝐼𝑦)))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3o 1086  w3a 1087   = wceq 1541  wcel 2106  {cab 2713  wral 3064  wrex 3073  {crab 3407  Vcvv 3445  [wsbc 3739  cdif 3907  cin 3909  wss 3910  𝒫 cpw 4560  {csn 4586  cfv 6496  (class class class)co 7357  cmpo 7359  Basecbs 17083  distcds 17142  TarskiGcstrkg 27369  TarskiGCcstrkgc 27370  TarskiGBcstrkgb 27371  TarskiGCBcstrkgcb 27372  Itvcitv 27375  LineGclng 27376
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2707  ax-sep 5256  ax-nul 5263
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2714  df-cleq 2728  df-clel 2814  df-ne 2944  df-ral 3065  df-rex 3074  df-rab 3408  df-v 3447  df-sbc 3740  df-dif 3913  df-un 3915  df-in 3917  df-ss 3927  df-nul 4283  df-if 4487  df-pw 4562  df-sn 4587  df-pr 4589  df-op 4593  df-uni 4866  df-br 5106  df-iota 6448  df-fv 6504  df-ov 7360  df-trkgb 27391  df-trkg 27395
This theorem is referenced by:  axtgcont  27411
  Copyright terms: Public domain W3C validator