Theorem isleagd

Description: Sufficient condition for "less than" angle relation, deduction version (Contributed by Thierry Arnoux, 12-Oct-2020)

	Ref	Expression
Hypotheses	isleag.p	$$⊢P={\mathrm{Base}}_G$$
	isleag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
	isleag.a	$$⊢\phi \to A\in P$$
	isleag.b	$$⊢\phi \to B\in P$$
	isleag.c	$$⊢\phi \to C\in P$$
	isleag.d	$$⊢\phi \to D\in P$$
	isleag.e	$$⊢\phi \to E\in P$$
	isleag.f	$$⊢\phi \to F\in P$$
	isleagd.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
	isleagd.x	$$⊢\phi \to X\in P$$
	isleagd.1	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
	isleagd.2	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEX”⟩$$
Assertion	isleagd	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\le }⟨“DEF”⟩$$

Proof

Step	Hyp	Ref	Expression
1		isleag.p	$$⊢P={\mathrm{Base}}_G$$
2		isleag.g	$$⊢\phi \to G\in {𝒢}_{\mathrm{Tarski}}$$
3		isleag.a	$$⊢\phi \to A\in P$$
4		isleag.b	$$⊢\phi \to B\in P$$
5		isleag.c	$$⊢\phi \to C\in P$$
6		isleag.d	$$⊢\phi \to D\in P$$
7		isleag.e	$$⊢\phi \to E\in P$$
8		isleag.f	$$⊢\phi \to F\in P$$
9		isleagd.s	$$⊢\underset{\dot{}}{\le }={\le }_{𝒢}^{\angle }\left(G\right)$$
10		isleagd.x	$$⊢\phi \to X\in P$$
11		isleagd.1	$$⊢\phi \to X{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
12		isleagd.2	$$⊢\phi \to ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEX”⟩$$
13	9	eqcomi	$$⊢{\le }_{𝒢}^{\angle }\left(G\right)=\underset{\dot{}}{\le }$$
14	13	a1i	$$⊢\phi \to {\le }_{𝒢}^{\angle }\left(G\right)=\underset{\dot{}}{\le }$$
15		simpr	$$⊢\left(\phi \wedge x=X\right)\to x=X$$
16	15	breq1d	$$⊢\left(\phi \wedge x=X\right)\to \left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\leftrightarrow X{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\right)$$
17		eqidd	$$⊢\left(\phi \wedge x=X\right)\to D=D$$
18		eqidd	$$⊢\left(\phi \wedge x=X\right)\to E=E$$
19	17 18 15	s3eqd	$$⊢\left(\phi \wedge x=X\right)\to ⟨“DEx”⟩=⟨“DEX”⟩$$
20	19	breq2d	$$⊢\left(\phi \wedge x=X\right)\to \left(⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\leftrightarrow ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEX”⟩\right)$$
21	16 20	anbi12d	$$⊢\left(\phi \wedge x=X\right)\to \left(\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\leftrightarrow \left(X{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEX”⟩\right)\right)$$
22	11 12	jca	$$⊢\phi \to \left(X{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEX”⟩\right)$$
23	10 21 22	rspcedvd	$$⊢\phi \to \exists x\in P\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)$$
24	1 2 3 4 5 6 7 8	isleag	$$⊢\phi \to \left(⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\leftrightarrow \exists x\in P\left(x{\in }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩\wedge ⟨“ABC”⟩{\sim }_{𝒢}^{\angle }\left(G\right)⟨“DEx”⟩\right)\right)$$
25	23 24	mpbird	$$⊢\phi \to ⟨“ABC”⟩{\le }_{𝒢}^{\angle }\left(G\right)⟨“DEF”⟩$$
26	14 25	breqdi	$$⊢\phi \to ⟨“ABC”⟩\underset{\dot{}}{\le }⟨“DEF”⟩$$