# Metamath Proof Explorer

## Theorem legso

Description: The "shorter than" relation induces an order on pairs. Remark 5.13 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

Ref Expression
Hypotheses legval.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
legval.d
legval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
legval.l
legval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
legso.a
legso.f
legso.l
legso.d
Assertion legso

### Proof

Step Hyp Ref Expression
1 legval.p ${⊢}{P}={\mathrm{Base}}_{{G}}$
2 legval.d
3 legval.i ${⊢}{I}=\mathrm{Itv}\left({G}\right)$
4 legval.l
5 legval.g ${⊢}{\phi }\to {G}\in {𝒢}_{\mathrm{Tarski}}$
6 legso.a
7 legso.f
8 legso.l
9 legso.d
10 neirr
11 10 intnan
12 5 adantr ${⊢}\left({\phi }\wedge {a}\in {E}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
17 simpllr
18 simplr
19 1 2 3 4 13 6 15 8 16 17 18 ltgov
20 11 19 mtbiri
21 simpr
22 21 21 breq12d
23 20 22 mtbird
24 simpr ${⊢}\left({\phi }\wedge {a}\in {E}\right)\to {a}\in {E}$
25 1 2 3 4 12 6 14 24 ltgseg
26 23 25 r19.29vva
29 simp-9r
30 simp-8r
31 simp-6r
32 simp-5r
33 simpllr
34 simplr
35 simp-10r
36 35 simpld
37 simp-7r
38 simp-4r
39 36 37 38 3brtr3d
44 1 2 3 4 28 6 41 8 43 29 30 ltgov
45 39 44 mpbid
46 45 simpld
47 35 simprd
48 simpr
49 47 38 48 3brtr3d
50 1 2 3 4 28 6 41 8 43 31 32 ltgov
51 49 50 mpbid
52 51 simpld
53 1 2 3 4 28 29 30 31 32 33 34 46 52 legtrd
61 simpr
62 60 61 breqtrrd
63 1 2 3 4 54 55 56 57 58 59 62 legtri3
64 45 simprd
66 65 neneqd
67 63 66 pm2.65da
68 67 neqned
69 1 2 3 4 28 6 41 8 43 29 30 ltgov
70 53 68 69 mpbir2and
71 70 37 48 3brtr4d
72 simp-5r
73 72 simp3d
75 1 2 3 4 27 6 40 74 ltgseg
76 71 75 r19.29vva
79 72 simp2d
80 1 2 3 4 77 6 78 79 ltgseg
81 76 80 r19.29vva
84 simplr1
85 1 2 3 4 82 6 83 84 ltgseg
86 81 85 r19.29vva
87 86 ex
88 26 87 ispod
90 simp-6r
91 simp-5r
92 simpllr
93 simplr
94 1 2 3 4 89 90 91 92 93 legtrid
97 1 2 3 4 89 6 95 8 96 90 91 legov3
98 1 2 3 4 89 6 95 8 96 92 93 legov3
99 97 98 orbi12d
100 94 99 mpbid
101 eqcom
102 101 orbi2i
103 102 orbi2i
104 df-3or
105 3orcomb
106 orordir
107 104 105 106 3bitr3ri
108 103 107 bitr3i
109 100 108 sylib
110 simp-4r
111 simpr
112 110 111 breq12d
113 110 111 eqeq12d
114 111 110 breq12d
115 112 113 114 3orbi123d
116 109 115 mpbird
117 5 ad2antrr ${⊢}\left(\left({\phi }\wedge {a}\in {E}\right)\wedge {b}\in {E}\right)\to {G}\in {𝒢}_{\mathrm{Tarski}}$
119 simpr ${⊢}\left(\left({\phi }\wedge {a}\in {E}\right)\wedge {b}\in {E}\right)\to {b}\in {E}$