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 = {Base}_{G}$
	legval.d	$⊢ \underset{˙}{-} = dist (G)$
	legval.i	$⊢ I = Itv (G)$
	legval.l	$⊢ \underset{˙}{\leq} = \leq_{𝒢} (G)$
	legval.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	legso.a	$⊢ E = \underset{˙}{-} [P \times P]$
	legso.f	$⊢ φ \to Fun \underset{˙}{-}$
	legso.l	$⊢ \underset{˙}{<} = ({\underset{˙}{\leq} ↾}_{E}) ∖ I$
	legso.d	$⊢ φ \to P \times P \subseteq dom \underset{˙}{-}$
Assertion	legso	$⊢ φ \to \underset{˙}{<} Or E$

Proof

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

Metamath Proof Explorer

Theorem legso

Proof