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

Theorem axtgcgrid 26301
 Description: Axiom of identity of congruence, Axiom A3 of [Schwabhauser] p. 10. (Contributed by Thierry Arnoux, 14-Mar-2019.)
Hypotheses
Ref Expression
axtrkg.p 𝑃 = (Base‘𝐺)
axtrkg.d = (dist‘𝐺)
axtrkg.i 𝐼 = (Itv‘𝐺)
axtrkg.g (𝜑𝐺 ∈ TarskiG)
axtgcgrid.1 (𝜑𝑋𝑃)
axtgcgrid.2 (𝜑𝑌𝑃)
axtgcgrid.3 (𝜑𝑍𝑃)
axtgcgrid.4 (𝜑 → (𝑋 𝑌) = (𝑍 𝑍))
Assertion
Ref Expression
axtgcgrid (𝜑𝑋 = 𝑌)

Proof of Theorem axtgcgrid
Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 26291 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 4158 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss1 4158 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
42, 3sstri 3926 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
51, 4eqsstri 3951 . . . 4 TarskiG ⊆ TarskiGC
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3915 . . 3 (𝜑𝐺 ∈ TarskiGC)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgc 26292 . . . . 5 (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))))
1211simprbi 500 . . . 4 (𝐺 ∈ TarskiGC → (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦)))
1312simprd 499 . . 3 (𝐺 ∈ TarskiGC → ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))
147, 13syl 17 . 2 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))
15 axtgcgrid.4 . 2 (𝜑 → (𝑋 𝑌) = (𝑍 𝑍))
16 axtgcgrid.1 . . 3 (𝜑𝑋𝑃)
17 axtgcgrid.2 . . 3 (𝜑𝑌𝑃)
18 axtgcgrid.3 . . 3 (𝜑𝑍𝑃)
19 oveq1 7152 . . . . . 6 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2019eqeq1d 2800 . . . . 5 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑧 𝑧) ↔ (𝑋 𝑦) = (𝑧 𝑧)))
21 eqeq1 2802 . . . . 5 (𝑥 = 𝑋 → (𝑥 = 𝑦𝑋 = 𝑦))
2220, 21imbi12d 348 . . . 4 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) ↔ ((𝑋 𝑦) = (𝑧 𝑧) → 𝑋 = 𝑦)))
23 oveq2 7153 . . . . . 6 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
2423eqeq1d 2800 . . . . 5 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑧 𝑧) ↔ (𝑋 𝑌) = (𝑧 𝑧)))
25 eqeq2 2810 . . . . 5 (𝑦 = 𝑌 → (𝑋 = 𝑦𝑋 = 𝑌))
2624, 25imbi12d 348 . . . 4 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑧 𝑧) → 𝑋 = 𝑦) ↔ ((𝑋 𝑌) = (𝑧 𝑧) → 𝑋 = 𝑌)))
27 id 22 . . . . . . 7 (𝑧 = 𝑍𝑧 = 𝑍)
2827, 27oveq12d 7163 . . . . . 6 (𝑧 = 𝑍 → (𝑧 𝑧) = (𝑍 𝑍))
2928eqeq2d 2809 . . . . 5 (𝑧 = 𝑍 → ((𝑋 𝑌) = (𝑧 𝑧) ↔ (𝑋 𝑌) = (𝑍 𝑍)))
3029imbi1d 345 . . . 4 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑧 𝑧) → 𝑋 = 𝑌) ↔ ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3122, 26, 30rspc3v 3585 . . 3 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) → ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3216, 17, 18, 31syl3anc 1368 . 2 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) → ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3314, 15, 32mp2d 49 1 (𝜑𝑋 = 𝑌)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 399   ∨ w3o 1083   = wceq 1538   ∈ wcel 2111  {cab 2776  ∀wral 3106  {crab 3110  Vcvv 3442  [wsbc 3722   ∖ cdif 3880   ∩ cin 3882  {csn 4528  ‘cfv 6332  (class class class)co 7145   ∈ cmpo 7147  Basecbs 16495  distcds 16586  TarskiGcstrkg 26268  TarskiGCcstrkgc 26269  TarskiGBcstrkgb 26270  TarskiGCBcstrkgcb 26271  Itvcitv 26274  LineGclng 26275 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 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-nul 5178 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-ral 3111  df-rex 3112  df-v 3444  df-sbc 3723  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4247  df-sn 4529  df-pr 4531  df-op 4535  df-uni 4805  df-br 5035  df-iota 6291  df-fv 6340  df-ov 7148  df-trkgc 26286  df-trkg 26291 This theorem is referenced by:  tgcgreqb  26319  tgcgrtriv  26322  tgsegconeq  26324  tgbtwntriv2  26325  tgbtwndiff  26344  tgifscgr  26346  tgbtwnxfr  26368  lnid  26408  tgbtwnconn1lem2  26411  tgbtwnconn1lem3  26412  legtri3  26428  legeq  26431  legbtwn  26432  mirreu3  26492  colmid  26526  krippenlem  26528  lmiisolem  26634  hypcgrlem1  26637  hypcgrlem2  26638  f1otrg  26709
 Copyright terms: Public domain W3C validator