legval

Description: Value of the less-than relationship. (Contributed by Thierry Arnoux, 21-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}$
Assertion	legval	$⊢ φ \to \underset{˙}{\leq} = \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\}$

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		elex	$⊢ G \in 𝒢_{Tarski} \to G \in V$
7		simp1	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to p = P$
8	7	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to P = p$
9		simp2	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to d = \underset{˙}{-}$
10	9	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to \underset{˙}{-} = d$
11	10	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x \underset{˙}{-} y = x d y$
12	11	eqeq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (f = x \underset{˙}{-} y \leftrightarrow f = x d y)$
13		simp3	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to i = I$
14	13	eqcomd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to I = i$
15	14	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x I y = x i y$
16	15	eleq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (z \in (x I y) \leftrightarrow z \in (x i y))$
17	10	oveqd	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to x \underset{˙}{-} z = x d z$
18	17	eqeq2d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (e = x \underset{˙}{-} z \leftrightarrow e = x d z)$
19	16 18	anbi12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((z \in (x I y) \land e = x \underset{˙}{-} z) \leftrightarrow (z \in (x i y) \land e = x d z))$
20	8 19	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z) \leftrightarrow \exists z \in p (z \in (x i y) \land e = x d z))$
21	12 20	anbi12d	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to ((f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \leftrightarrow (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z)))$
22	8 21	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \leftrightarrow \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z)))$
23	8 22	rexeqbidv	$⊢ (p = P \land d = \underset{˙}{-} \land i = I) \to (\exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \leftrightarrow \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z)))$
24	1 2 3 23	sbcie3s	$⊢ g = G \to (\underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z)) \leftrightarrow \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)))$
25	24	opabbidv	$⊢ g = G \to \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\} = \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\}$
26		df-leg	$⊢ \leq_{𝒢} = (g \in V ⟼ \{⟨e, f⟩ \| \underset{˙}{[} {Base}_{g} / p \underset{˙}{]} \underset{˙}{[} dist (g) / d \underset{˙}{]} \underset{˙}{[} Itv (g) / i \underset{˙}{]} \exists x \in p \exists y \in p (f = x d y \land \exists z \in p (z \in (x i y) \land e = x d z))\})$
27	2	fvexi	$⊢ \underset{˙}{-} \in V$
28	27	imaex	$⊢ \underset{˙}{-} [P \times P] \in V$
29		p0ex	$⊢ \{\emptyset\} \in V$
30	28 29	unex	$⊢ \underset{˙}{-} [P \times P] \cup \{\emptyset\} \in V$
31	30	a1i	$⊢ ⊤ \to \underset{˙}{-} [P \times P] \cup \{\emptyset\} \in V$
32		simprr	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to e = x \underset{˙}{-} d$
33		ovima0	$⊢ (x \in P \land d \in P) \to x \underset{˙}{-} d \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
34	33	ad5ant14	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to x \underset{˙}{-} d \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
35	32 34	eqeltrd	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
36		simpllr	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))$
37	36	simpld	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to f = x \underset{˙}{-} y$
38		ovima0	$⊢ (x \in P \land y \in P) \to x \underset{˙}{-} y \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
39	38	ad3antrrr	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to x \underset{˙}{-} y \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
40	37 39	eqeltrd	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
41	35 40	jca	$⊢ ((((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \land d \in P) \land (d \in (x I y) \land e = x \underset{˙}{-} d)) \to (e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}) \land f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}))$
42		simprr	$⊢ ((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)$
43		eleq1w	$⊢ z = d \to (z \in (x I y) \leftrightarrow d \in (x I y))$
44		oveq2	$⊢ z = d \to x \underset{˙}{-} z = x \underset{˙}{-} d$
45	44	eqeq2d	$⊢ z = d \to (e = x \underset{˙}{-} z \leftrightarrow e = x \underset{˙}{-} d)$
46	43 45	anbi12d	$⊢ z = d \to ((z \in (x I y) \land e = x \underset{˙}{-} z) \leftrightarrow (d \in (x I y) \land e = x \underset{˙}{-} d))$
47	46	cbvrexvw	$⊢ \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z) \leftrightarrow \exists d \in P (d \in (x I y) \land e = x \underset{˙}{-} d)$
48	42 47	sylib	$⊢ ((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to \exists d \in P (d \in (x I y) \land e = x \underset{˙}{-} d)$
49	41 48	r19.29a	$⊢ ((x \in P \land y \in P) \land (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to (e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}) \land f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}))$
50	49	ex	$⊢ (x \in P \land y \in P) \to ((f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \to (e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}) \land f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})))$
51	50	rexlimivv	$⊢ \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \to (e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}) \land f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}))$
52	51	adantl	$⊢ (⊤ \land \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to (e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}) \land f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\}))$
53	52	simpld	$⊢ (⊤ \land \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to e \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
54	52	simprd	$⊢ (⊤ \land \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))) \to f \in (\underset{˙}{-} [P \times P] \cup \{\emptyset\})$
55	31 31 53 54	opabex2	$⊢ ⊤ \to \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\} \in V$
56	55	mptru	$⊢ \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\} \in V$
57	25 26 56	fvmpt	$⊢ G \in V \to \leq_{𝒢} (G) = \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\}$
58	5 6 57	3syl	$⊢ φ \to \leq_{𝒢} (G) = \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\}$
59	4 58	syl5eq	$⊢ φ \to \underset{˙}{\leq} = \{⟨e, f⟩ \| \exists x \in P \exists y \in P (f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z))\}$

Metamath Proof Explorer

Theorem legval

Proof