Theorem legid

Description: Reflexivity of the less-than relationship. Proposition 5.7 of Schwabhauser p. 42. (Contributed by Thierry Arnoux, 27-Jun-2019)

	Ref	Expression
Hypotheses	legval.p	$$⊢P={\mathrm{Base}}_G$$
	legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
	legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
	legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
	legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	legid.a	$$⊢\phi \to A\in P$$
	legid.b	$$⊢\phi \to B\in P$$
Assertion	legid	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		legval.p	$$⊢P={\mathrm{Base}}_G$$
2		legval.d	$$⊢\underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
3		legval.i	$$⊢I=\mathrm{Itv}\left(G\right)$$
4		legval.l	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}\left(G\right)$$
5		legval.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
6		legid.a	$$⊢\phi \to A\in P$$
7		legid.b	$$⊢\phi \to B\in P$$
8	1 2 3 5 6 7	tgbtwntriv2	$$⊢\phi \to B\in \left(AIB\right)$$
9		eqidd	$$⊢\phi \to A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B$$
10		eleq1	$$⊢x=B\to \left(x\in \left(AIB\right)\leftrightarrow B\in \left(AIB\right)\right)$$
11		oveq2	$$⊢x=B\to A\underset{\dot{}}{-}x=A\underset{\dot{}}{-}B$$
12	11	eqeq2d	$$⊢x=B\to \left(A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\leftrightarrow A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)$$
13	10 12	anbi12d	$$⊢x=B\to \left(\left(x\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)\leftrightarrow \left(B\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)\right)$$
14	13	rspcev	$$⊢\left(B\in P\wedge \left(B\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}B\right)\right)\to \exists x\in P\left(x\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)$$
15	7 8 9 14	syl12anc	$$⊢\phi \to \exists x\in P\left(x\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)$$
16	1 2 3 4 5 6 7 6 7	legov	$$⊢\phi \to \left(\left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}B\right)\leftrightarrow \exists x\in P\left(x\in \left(AIB\right)\wedge A\underset{\dot{}}{-}B=A\underset{\dot{}}{-}x\right)\right)$$
17	15 16	mpbird	$$⊢\phi \to \left(A\underset{\dot{}}{-}B\right)\underset{\dot{}}{\le }\left(A\underset{\dot{}}{-}B\right)$$