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

Theorem axtgcgrrflx 26270
 Description: Axiom of reflexivity of congruence, Axiom A1 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)
axtgcgrrflx.1 (𝜑𝑋𝑃)
axtgcgrrflx.2 (𝜑𝑌𝑃)
Assertion
Ref Expression
axtgcgrrflx (𝜑 → (𝑋 𝑌) = (𝑌 𝑋))

Proof of Theorem axtgcgrrflx
Dummy variables 𝑓 𝑖 𝑝 𝑥 𝑦 𝑧 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 df-trkg 26261 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})}))
2 inss1 4155 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ (TarskiGC ∩ TarskiGB)
3 inss1 4155 . . . . . 6 (TarskiGC ∩ TarskiGB) ⊆ TarskiGC
42, 3sstri 3924 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓[(Base‘𝑓) / 𝑝][(Itv‘𝑓) / 𝑖](LineG‘𝑓) = (𝑥𝑝, 𝑦 ∈ (𝑝 ∖ {𝑥}) ↦ {𝑧𝑝 ∣ (𝑧 ∈ (𝑥𝑖𝑦) ∨ 𝑥 ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (𝑥𝑖𝑧))})})) ⊆ TarskiGC
51, 4eqsstri 3949 . . . 4 TarskiG ⊆ TarskiGC
6 axtrkg.g . . . 4 (𝜑𝐺 ∈ TarskiG)
75, 6sseldi 3913 . . 3 (𝜑𝐺 ∈ TarskiGC)
8 axtrkg.p . . . . . 6 𝑃 = (Base‘𝐺)
9 axtrkg.d . . . . . 6 = (dist‘𝐺)
10 axtrkg.i . . . . . 6 𝐼 = (Itv‘𝐺)
118, 9, 10istrkgc 26262 . . . . 5 (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦))))
1211simprbi 500 . . . 4 (𝐺 ∈ TarskiGC → (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) ∧ ∀𝑥𝑃𝑦𝑃𝑧𝑃 ((𝑥 𝑦) = (𝑧 𝑧) → 𝑥 = 𝑦)))
1312simpld 498 . . 3 (𝐺 ∈ TarskiGC → ∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥))
147, 13syl 17 . 2 (𝜑 → ∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥))
15 axtgcgrrflx.1 . . 3 (𝜑𝑋𝑃)
16 axtgcgrrflx.2 . . 3 (𝜑𝑌𝑃)
17 oveq1 7147 . . . . 5 (𝑥 = 𝑋 → (𝑥 𝑦) = (𝑋 𝑦))
18 oveq2 7148 . . . . 5 (𝑥 = 𝑋 → (𝑦 𝑥) = (𝑦 𝑋))
1917, 18eqeq12d 2814 . . . 4 (𝑥 = 𝑋 → ((𝑥 𝑦) = (𝑦 𝑥) ↔ (𝑋 𝑦) = (𝑦 𝑋)))
20 oveq2 7148 . . . . 5 (𝑦 = 𝑌 → (𝑋 𝑦) = (𝑋 𝑌))
21 oveq1 7147 . . . . 5 (𝑦 = 𝑌 → (𝑦 𝑋) = (𝑌 𝑋))
2220, 21eqeq12d 2814 . . . 4 (𝑦 = 𝑌 → ((𝑋 𝑦) = (𝑦 𝑋) ↔ (𝑋 𝑌) = (𝑌 𝑋)))
2319, 22rspc2v 3581 . . 3 ((𝑋𝑃𝑌𝑃) → (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) → (𝑋 𝑌) = (𝑌 𝑋)))
2415, 16, 23syl2anc 587 . 2 (𝜑 → (∀𝑥𝑃𝑦𝑃 (𝑥 𝑦) = (𝑦 𝑥) → (𝑋 𝑌) = (𝑌 𝑋)))
2514, 24mpd 15 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 3441  [wsbc 3720   ∖ cdif 3878   ∩ cin 3880  {csn 4525  ‘cfv 6327  (class class class)co 7140   ∈ cmpo 7142  Basecbs 16482  distcds 16573  TarskiGcstrkg 26238  TarskiGCcstrkgc 26239  TarskiGBcstrkgb 26240  TarskiGCBcstrkgcb 26241  Itvcitv 26244  LineGclng 26245 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 5175 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 3443  df-sbc 3721  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-br 5032  df-iota 6286  df-fv 6335  df-ov 7143  df-trkgc 26256  df-trkg 26261 This theorem is referenced by:  tgcgrcomimp  26285  tgcgrcomr  26286  tgcgrcoml  26287  tgcgrcomlr  26288  tgbtwnconn1lem1  26380  tgbtwnconn1lem2  26381  tgbtwnconn1lem3  26382  miriso  26478  symquadlem  26497  midexlem  26500  footexALT  26526  footexlem1  26527  footexlem2  26528  colperpexlem1  26538  opphllem  26543  cgraswap  26628  isoas  26672  f1otrg  26679
 Copyright terms: Public domain W3C validator