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

Theorem tgbtwnconn1lem2 23802
 Description: Lemma for tgbtwnconn1 23804 (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
tgbtwnconn1lem2

Proof of Theorem tgbtwnconn1lem2
StepHypRef Expression
1 tgbtwnconn1.p . . . . 5
2 tgbtwnconn1.m . . . . 5
3 tgbtwnconn1.i . . . . 5 Itv
4 tgbtwnconn1.g . . . . 5 TarskiG
5 tgbtwnconn1.e . . . . 5
6 tgbtwnconn1.f . . . . 5
71, 2, 3, 4, 5, 6axtgcgrrflx 23702 . . . 4
94adantr 465 . . . . . . 7 TarskiG
105adantr 465 . . . . . . 7
11 tgbtwnconn1.h . . . . . . . 8
1211adantr 465 . . . . . . 7
13 tgbtwnconn1.c . . . . . . . 8
1413adantr 465 . . . . . . 7
15 tgbtwnconn1.10 . . . . . . . . 9
1615adantr 465 . . . . . . . 8
17 simpr 461 . . . . . . . . 9
1817oveq1d 6309 . . . . . . . 8
1916, 18eqtrd 2508 . . . . . . 7
201, 2, 3, 9, 10, 12, 14, 19axtgcgrid 23703 . . . . . 6
21 tgbtwnconn1.a . . . . . . . 8
22 tgbtwnconn1.b . . . . . . . 8
23 tgbtwnconn1.d . . . . . . . 8
24 tgbtwnconn1.1 . . . . . . . 8
25 tgbtwnconn1.2 . . . . . . . 8
26 tgbtwnconn1.3 . . . . . . . 8
27 tgbtwnconn1.j . . . . . . . 8
28 tgbtwnconn1.4 . . . . . . . 8
29 tgbtwnconn1.5 . . . . . . . 8
30 tgbtwnconn1.6 . . . . . . . 8
31 tgbtwnconn1.7 . . . . . . . 8
32 tgbtwnconn1.8 . . . . . . . 8
33 tgbtwnconn1.9 . . . . . . . 8
34 tgbtwnconn1.11 . . . . . . . 8
351, 3, 4, 21, 22, 13, 23, 24, 25, 26, 2, 5, 6, 11, 27, 28, 29, 30, 31, 32, 33, 15, 34tgbtwnconn1lem1 23801 . . . . . . 7
3635adantr 465 . . . . . 6
3720, 36eqtrd 2508 . . . . 5
3837oveq2d 6310 . . . 4
3934adantr 465 . . . 4
4017oveq1d 6309 . . . 4
4138, 39, 403eqtrd 2512 . . 3
428, 41eqtrd 2508 . 2
434adantr 465 . . 3 TarskiG
4822adantr 465 . . . 4
4927adantr 465 . . . 4
50 simpr 461 . . . 4
511, 2, 3, 4, 21, 22, 13, 6, 25, 29tgbtwnexch3 23728 . . . . 5
5251adantr 465 . . . 4
5335oveq2d 6310 . . . . . . . 8
5430, 53eleqtrd 2557 . . . . . . 7
551, 2, 3, 4, 21, 23, 5, 27, 28, 54tgbtwnexch3 23728 . . . . . 6
561, 2, 3, 4, 23, 5, 27, 55tgbtwncom 23722 . . . . 5
5756adantr 465 . . . 4
5835adantr 465 . . . . . 6
5958oveq2d 6310 . . . . 5
6015adantr 465 . . . . 5
611, 2, 3, 43, 45, 49axtgcgrrflx 23702 . . . . 5
6259, 60, 613eqtr3d 2516 . . . 4
6333, 32eqtr4d 2511 . . . . 5
6463adantr 465 . . . 4
651, 2, 3, 4, 21, 22, 23, 5, 26, 28tgbtwnexch3 23728 . . . . . 6
6665adantr 465 . . . . 5
671, 2, 3, 4, 21, 13, 6, 27, 29, 31tgbtwnexch3 23728 . . . . . . 7
681, 2, 3, 4, 13, 6, 27, 67tgbtwncom 23722 . . . . . 6
6968adantr 465 . . . . 5
701, 2, 3, 4, 27, 6axtgcgrrflx 23702 . . . . . . 7
7170, 34eqtr2d 2509 . . . . . 6
7271adantr 465 . . . . 5
731, 2, 3, 4, 13, 6, 5, 23, 63tgcgrcomlr 23714 . . . . . . 7
7473adantr 465 . . . . . 6
7574eqcomd 2475 . . . . 5
761, 2, 3, 43, 48, 46, 45, 49, 44, 47, 66, 69, 72, 75tgcgrextend 23719 . . . 4
771, 2, 3, 43, 47, 45axtgcgrrflx 23702 . . . 4
781, 2, 3, 43, 48, 47, 44, 49, 45, 46, 45, 47, 50, 52, 57, 62, 64, 76, 77axtg5seg 23705 . . 3
791, 2, 3, 43, 44, 45, 46, 47, 78tgcgrcomlr 23714 . 2
8042, 79pm2.61dane 2785 1
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 369   wceq 1379   wcel 1767   wne 2662  cfv 5593  (class class class)co 6294  cbs 14502  cds 14576  TarskiGcstrkg 23668  Itvcitv 23675 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-nul 4581 This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-ral 2822  df-rex 2823  df-rab 2826  df-v 3120  df-sbc 3337  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-pw 4017  df-sn 4033  df-pr 4035  df-op 4039  df-uni 4251  df-br 4453  df-iota 5556  df-fv 5601  df-ov 6297  df-trkgc 23687  df-trkgb 23688  df-trkgcb 23689  df-trkg 23693 This theorem is referenced by:  tgbtwnconn1lem3  23803
 Copyright terms: Public domain W3C validator