Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  tgbtwnconn1lem1 Structured version   Unicode version

Theorem tgbtwnconn1lem1 23124
 Description: Lemma for tgbtwnconn1 23127 (Contributed by Thierry Arnoux, 30-Apr-2019.)
Hypotheses
Ref Expression
tgbtwnconn1.p
tgbtwnconn1.i Itv
tgbtwnconn1.g TarskiG
tgbtwnconn1.a
tgbtwnconn1.b
tgbtwnconn1.c
tgbtwnconn1.d
tgbtwnconn1.1
tgbtwnconn1.2
tgbtwnconn1.3
tgbtwnconn1.m
tgbtwnconn1.e
tgbtwnconn1.f
tgbtwnconn1.h
tgbtwnconn1.j
tgbtwnconn1.4
tgbtwnconn1.5
tgbtwnconn1.6
tgbtwnconn1.7
tgbtwnconn1.8
tgbtwnconn1.9
tgbtwnconn1.10
tgbtwnconn1.11
Assertion
Ref Expression
tgbtwnconn1lem1

Proof of Theorem tgbtwnconn1lem1
StepHypRef Expression
1 tgbtwnconn1.p . 2
2 tgbtwnconn1.m . 2
3 tgbtwnconn1.i . 2 Itv
4 tgbtwnconn1.g . 2 TarskiG
5 tgbtwnconn1.b . 2
6 tgbtwnconn1.j . 2
7 tgbtwnconn1.a . 2
8 tgbtwnconn1.h . 2
9 tgbtwnconn1.1 . 2
10 tgbtwnconn1.e . . 3
11 tgbtwnconn1.d . . . 4
12 tgbtwnconn1.3 . . . 4
13 tgbtwnconn1.4 . . . 4
141, 2, 3, 4, 7, 5, 11, 10, 12, 13tgbtwnexch 23069 . . 3
15 tgbtwnconn1.6 . . 3
161, 2, 3, 4, 7, 5, 10, 8, 14, 15tgbtwnexch 23069 . 2
17 tgbtwnconn1.f . . 3
18 tgbtwnconn1.c . . . 4
19 tgbtwnconn1.2 . . . 4
20 tgbtwnconn1.5 . . . 4
211, 2, 3, 4, 7, 5, 18, 17, 19, 20tgbtwnexch 23069 . . 3
22 tgbtwnconn1.7 . . 3
231, 2, 3, 4, 7, 5, 17, 6, 21, 22tgbtwnexch 23069 . 2
241, 2, 3, 4, 7, 5, 10, 8, 14, 15tgbtwnexch3 23065 . . 3
251, 2, 3, 4, 7, 17, 6, 22tgbtwncom 23059 . . . . . . 7
261, 2, 3, 4, 7, 18, 17, 20tgbtwncom 23059 . . . . . . 7
271, 2, 3, 4, 6, 17, 18, 7, 25, 26tgbtwnexch2 23067 . . . . . 6
281, 2, 3, 4, 6, 18, 7, 27tgbtwncom 23059 . . . . 5
291, 2, 3, 4, 7, 5, 18, 6, 19, 28tgbtwnexch3 23065 . . . 4
301, 2, 3, 4, 5, 18, 6, 29tgbtwncom 23059 . . 3
311, 2, 3, 4, 7, 5, 11, 10, 12, 13tgbtwnexch3 23065 . . . 4
321, 2, 3, 4, 7, 18, 17, 6, 20, 22tgbtwnexch3 23065 . . . . 5
331, 2, 3, 4, 18, 17, 6, 32tgbtwncom 23059 . . . 4
341, 2, 3, 4, 6, 17axtgcgrrflx 23039 . . . . 5
35 tgbtwnconn1.11 . . . . 5
3634, 35eqtr2d 2493 . . . 4
37 tgbtwnconn1.8 . . . . . 6
38 tgbtwnconn1.9 . . . . . 6
3937, 38eqtr4d 2495 . . . . 5
401, 2, 3, 4, 10, 11, 18, 17, 39tgcgrcomlr 23051 . . . 4
411, 2, 3, 4, 5, 11, 10, 6, 17, 18, 31, 33, 36, 40tgcgrextend 23056 . . 3
42 tgbtwnconn1.10 . . . 4
431, 2, 3, 4, 18, 5axtgcgrrflx 23039 . . . 4
4442, 43eqtr4d 2495 . . 3
451, 2, 3, 4, 5, 10, 8, 6, 18, 5, 24, 30, 41, 44tgcgrextend 23056 . 2
461, 2, 3, 4, 5, 6axtgcgrrflx 23039 . 2
471, 2, 3, 4, 5, 6, 5, 7, 8, 6, 9, 16, 23, 45, 46tgsegconeq 23057 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wceq 1370   wcel 1758   wne 2644  cfv 5516  (class class class)co 6190  cbs 14276  cds 14349  TarskiGcstrkg 23005  Itvcitv 23012 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1952  ax-ext 2430  ax-nul 4519 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2264  df-clab 2437  df-cleq 2443  df-clel 2446  df-nfc 2601  df-ne 2646  df-ral 2800  df-rex 2801  df-rab 2804  df-v 3070  df-sbc 3285  df-dif 3429  df-un 3431  df-in 3433  df-ss 3440  df-nul 3736  df-if 3890  df-pw 3960  df-sn 3976  df-pr 3978  df-op 3982  df-uni 4190  df-br 4391  df-iota 5479  df-fv 5524  df-ov 6193  df-trkgc 23024  df-trkgb 23025  df-trkgcb 23026  df-trkg 23030 This theorem is referenced by:  tgbtwnconn1lem2  23125  tgbtwnconn1lem3  23126
 Copyright terms: Public domain W3C validator