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

Theorem legtri3 23720
 Description: Equality from the less-than relationship. Proposition 5.9 of [Schwabhauser] p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019.)
Hypotheses
Ref Expression
legval.p
legval.d
legval.i Itv
legval.l ≤G
legval.g TarskiG
legid.a
legid.b
legtrd.c
legtrd.d
legtri3.1
legtri3.2
Assertion
Ref Expression
legtri3

Proof of Theorem legtri3
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpllr 758 . . . . 5
21simprd 463 . . . 4
3 legval.p . . . . . 6
4 legval.d . . . . . 6
5 legval.i . . . . . 6 Itv
6 legval.g . . . . . . 7 TarskiG
76ad4antr 731 . . . . . 6 TarskiG
8 simp-4r 766 . . . . . 6
9 legtrd.d . . . . . . 7
109ad4antr 731 . . . . . 6
11 legtrd.c . . . . . . 7
1211ad4antr 731 . . . . . 6
131simpld 459 . . . . . . 7
143, 4, 5, 7, 12, 8, 10, 13tgbtwncom 23623 . . . . . 6
15 simpr 461 . . . . . . . . 9
1615simpld 459 . . . . . . . 8
17 simplr 754 . . . . . . . . . 10
18 legid.b . . . . . . . . . . 11
1918ad4antr 731 . . . . . . . . . 10
20 legid.a . . . . . . . . . . . 12
2120ad4antr 731 . . . . . . . . . . 11
223, 4, 5, 7, 12, 10, 17, 16tgbtwncom 23623 . . . . . . . . . . . 12
233, 4, 5, 7, 17, 10, 8, 12, 22, 14tgbtwnexch2 23631 . . . . . . . . . . 11
243, 4, 5, 7, 19, 21tgbtwntriv1 23626 . . . . . . . . . . 11
2515simprd 463 . . . . . . . . . . . 12
263, 4, 5, 7, 12, 17, 21, 19, 25tgcgrcomlr 23615 . . . . . . . . . . 11
272eqcomd 2475 . . . . . . . . . . . 12
283, 4, 5, 7, 12, 8, 21, 19, 27tgcgrcomlr 23615 . . . . . . . . . . 11
293, 4, 5, 7, 17, 8, 12, 19, 19, 21, 23, 24, 26, 28tgcgrsub 23645 . . . . . . . . . 10
303, 4, 5, 7, 17, 8, 19, 29axtgcgrid 23604 . . . . . . . . 9
3130oveq2d 6299 . . . . . . . 8
3216, 31eleqtrd 2557 . . . . . . 7
333, 4, 5, 7, 12, 10, 8, 32tgbtwncom 23623 . . . . . 6
343, 4, 5, 7, 8, 10, 12, 14, 33tgbtwnswapid 23627 . . . . 5
3534oveq2d 6299 . . . 4
362, 35eqtrd 2508 . . 3
37 legtri3.2 . . . . 5
38 legval.l . . . . . 6 ≤G
393, 4, 5, 38, 6, 11, 9, 20, 18legov2 23716 . . . . 5
4037, 39mpbid 210 . . . 4