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

Theorem axtgcgrid 25561
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 25551 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 3976 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss1 3976 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
42, 3sstri 3753 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
51, 4eqsstri 3776 . . . 4 TarskiG ⊆ TarskiGC
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3742 . . 3 (𝜑𝐺 ∈ TarskiGC)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgc 25552 . . . . 5 (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))))
1211simprbi 483 . . . 4 (𝐺 ∈ TarskiGC → (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦)))
1312simprd 482 . . 3 (𝐺 ∈ TarskiGC → ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))
147, 13syl 17 . 2 (𝜑 → ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))
15 axtgcgrid.4 . 2 (𝜑 → (𝑋 𝑌) = (𝑍 𝑍))
16 axtgcgrid.1 . . 3 (𝜑𝑋𝑃)
17 axtgcgrid.2 . . 3 (𝜑𝑌𝑃)
18 axtgcgrid.3 . . 3 (𝜑𝑍𝑃)
19 oveq1 6820 . . . . . 6 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
2019eqeq1d 2762 . . . . 5 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑧 𝑧) ↔ (𝑋 𝑦) = (𝑧 𝑧)))
21 eqeq1 2764 . . . . 5 (𝑥 = 𝑋 → (𝑥 = 𝑦𝑋 = 𝑦))
2220, 21imbi12d 333 . . . 4 (𝑥 = 𝑋 → (((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) ↔ ((𝑋 𝑦) = (𝑧 𝑧) → 𝑋 = 𝑦)))
23 oveq2 6821 . . . . . 6 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
2423eqeq1d 2762 . . . . 5 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑧 𝑧) ↔ (𝑋 𝑌) = (𝑧 𝑧)))
25 eqeq2 2771 . . . . 5 (𝑦 = 𝑌 → (𝑋 = 𝑦𝑋 = 𝑌))
2624, 25imbi12d 333 . . . 4 (𝑦 = 𝑌 → (((𝑋 𝑦) = (𝑧 𝑧) → 𝑋 = 𝑦) ↔ ((𝑋 𝑌) = (𝑧 𝑧) → 𝑋 = 𝑌)))
27 id 22 . . . . . . 7 (𝑧 = 𝑍𝑧 = 𝑍)
2827, 27oveq12d 6831 . . . . . 6 (𝑧 = 𝑍 → (𝑧 𝑧) = (𝑍 𝑍))
2928eqeq2d 2770 . . . . 5 (𝑧 = 𝑍 → ((𝑋 𝑌) = (𝑧 𝑧) ↔ (𝑋 𝑌) = (𝑍 𝑍)))
3029imbi1d 330 . . . 4 (𝑧 = 𝑍 → (((𝑋 𝑌) = (𝑧 𝑧) → 𝑋 = 𝑌) ↔ ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3122, 26, 30rspc3v 3464 . . 3 ((𝑋𝑃𝑌𝑃𝑍𝑃) → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) → ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3216, 17, 18, 31syl3anc 1477 . 2 (𝜑 → (∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦) → ((𝑋 𝑌) = (𝑍 𝑍) → 𝑋 = 𝑌)))
3314, 15, 32mp2d 49 1 (𝜑𝑋 = 𝑌)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 383  w3o 1071   = wceq 1632  wcel 2139  {cab 2746  wral 3050  {crab 3054  Vcvv 3340  [wsbc 3576  cdif 3712  cin 3714  {csn 4321  cfv 6049  (class class class)co 6813  cmpt2 6815  Basecbs 16059  distcds 16152  TarskiGcstrkg 25528  TarskiGCcstrkgc 25529  TarskiGBcstrkgb 25530  TarskiGCBcstrkgcb 25531  Itvcitv 25534  LineGclng 25535
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740  ax-nul 4941
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-eu 2611  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-ral 3055  df-rex 3056  df-rab 3059  df-v 3342  df-sbc 3577  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-uni 4589  df-br 4805  df-iota 6012  df-fv 6057  df-ov 6816  df-trkgc 25546  df-trkg 25551
This theorem is referenced by:  tgcgreqb  25575  tgcgrtriv  25578  tgsegconeq  25580  tgbtwntriv2  25581  tgbtwndiff  25600  tgifscgr  25602  tgbtwnxfr  25624  lnid  25664  tgbtwnconn1lem2  25667  tgbtwnconn1lem3  25668  legtri3  25684  legeq  25687  legbtwn  25688  mirreu3  25748  colmid  25782  krippenlem  25784  lmiisolem  25887  hypcgrlem1  25890  hypcgrlem2  25891  f1otrg  25950
  Copyright terms: Public domain W3C validator