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

Theorem axtgcgrrflx 28182
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 28173 . . . . 5 TarskiG = ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})}))
2 inss1 4220 . . . . . 6 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† (TarskiGC ∩ TarskiGB)
3 inss1 4220 . . . . . 6 (TarskiGC ∩ TarskiGB) βŠ† TarskiGC
42, 3sstri 3983 . . . . 5 ((TarskiGC ∩ TarskiGB) ∩ (TarskiGCB ∩ {𝑓 ∣ [(Baseβ€˜π‘“) / 𝑝][(Itvβ€˜π‘“) / 𝑖](LineGβ€˜π‘“) = (π‘₯ ∈ 𝑝, 𝑦 ∈ (𝑝 βˆ– {π‘₯}) ↦ {𝑧 ∈ 𝑝 ∣ (𝑧 ∈ (π‘₯𝑖𝑦) ∨ π‘₯ ∈ (𝑧𝑖𝑦) ∨ 𝑦 ∈ (π‘₯𝑖𝑧))})})) βŠ† TarskiGC
51, 4eqsstri 4008 . . . 4 TarskiG βŠ† TarskiGC
6 axtrkg.g . . . 4 (πœ‘ β†’ 𝐺 ∈ TarskiG)
75, 6sselid 3972 . . 3 (πœ‘ β†’ 𝐺 ∈ TarskiGC)
8 axtrkg.p . . . . . 6 𝑃 = (Baseβ€˜πΊ)
9 axtrkg.d . . . . . 6 βˆ’ = (distβ€˜πΊ)
10 axtrkg.i . . . . . 6 𝐼 = (Itvβ€˜πΊ)
118, 9, 10istrkgc 28174 . . . . 5 (𝐺 ∈ TarskiGC ↔ (𝐺 ∈ V ∧ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 ((π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑧) β†’ π‘₯ = 𝑦))))
1211simprbi 496 . . . 4 (𝐺 ∈ TarskiGC β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯) ∧ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 βˆ€π‘§ ∈ 𝑃 ((π‘₯ βˆ’ 𝑦) = (𝑧 βˆ’ 𝑧) β†’ π‘₯ = 𝑦)))
1312simpld 494 . . 3 (𝐺 ∈ TarskiGC β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯))
147, 13syl 17 . 2 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯))
15 axtgcgrrflx.1 . . 3 (πœ‘ β†’ 𝑋 ∈ 𝑃)
16 axtgcgrrflx.2 . . 3 (πœ‘ β†’ π‘Œ ∈ 𝑃)
17 oveq1 7408 . . . . 5 (π‘₯ = 𝑋 β†’ (π‘₯ βˆ’ 𝑦) = (𝑋 βˆ’ 𝑦))
18 oveq2 7409 . . . . 5 (π‘₯ = 𝑋 β†’ (𝑦 βˆ’ π‘₯) = (𝑦 βˆ’ 𝑋))
1917, 18eqeq12d 2740 . . . 4 (π‘₯ = 𝑋 β†’ ((π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯) ↔ (𝑋 βˆ’ 𝑦) = (𝑦 βˆ’ 𝑋)))
20 oveq2 7409 . . . . 5 (𝑦 = π‘Œ β†’ (𝑋 βˆ’ 𝑦) = (𝑋 βˆ’ π‘Œ))
21 oveq1 7408 . . . . 5 (𝑦 = π‘Œ β†’ (𝑦 βˆ’ 𝑋) = (π‘Œ βˆ’ 𝑋))
2220, 21eqeq12d 2740 . . . 4 (𝑦 = π‘Œ β†’ ((𝑋 βˆ’ 𝑦) = (𝑦 βˆ’ 𝑋) ↔ (𝑋 βˆ’ π‘Œ) = (π‘Œ βˆ’ 𝑋)))
2319, 22rspc2v 3614 . . 3 ((𝑋 ∈ 𝑃 ∧ π‘Œ ∈ 𝑃) β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯) β†’ (𝑋 βˆ’ π‘Œ) = (π‘Œ βˆ’ 𝑋)))
2415, 16, 23syl2anc 583 . 2 (πœ‘ β†’ (βˆ€π‘₯ ∈ 𝑃 βˆ€π‘¦ ∈ 𝑃 (π‘₯ βˆ’ 𝑦) = (𝑦 βˆ’ π‘₯) β†’ (𝑋 βˆ’ π‘Œ) = (π‘Œ βˆ’ 𝑋)))
2514, 24mpd 15 1 (πœ‘ β†’ (𝑋 βˆ’ π‘Œ) = (π‘Œ βˆ’ 𝑋))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ∧ wa 395   ∨ w3o 1083   = wceq 1533   ∈ wcel 2098  {cab 2701  βˆ€wral 3053  {crab 3424  Vcvv 3466  [wsbc 3769   βˆ– cdif 3937   ∩ cin 3939  {csn 4620  β€˜cfv 6533  (class class class)co 7401   ∈ cmpo 7403  Basecbs 17143  distcds 17205  TarskiGcstrkg 28147  TarskiGCcstrkgc 28148  TarskiGBcstrkgb 28149  TarskiGCBcstrkgcb 28150  Itvcitv 28153  LineGclng 28154
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2695  ax-nul 5296
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-ne 2933  df-ral 3054  df-rab 3425  df-v 3468  df-sbc 3770  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-uni 4900  df-br 5139  df-iota 6485  df-fv 6541  df-ov 7404  df-trkgc 28168  df-trkg 28173
This theorem is referenced by:  tgcgrcomimp  28197  tgcgrcomr  28198  tgcgrcoml  28199  tgcgrcomlr  28200  tgbtwnconn1lem1  28292  tgbtwnconn1lem2  28293  tgbtwnconn1lem3  28294  miriso  28390  symquadlem  28409  midexlem  28412  footexALT  28438  footexlem1  28439  footexlem2  28440  colperpexlem1  28450  opphllem  28455  cgraswap  28540  isoas  28584  f1otrg  28591
  Copyright terms: Public domain W3C validator