legov

Description: Value of the less-than relationship. Definition 5.4 of Schwabhauser p. 41. (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}$
	legov.a	$⊢ φ \to A \in P$
	legov.b	$⊢ φ \to B \in P$
	legov.c	$⊢ φ \to C \in P$
	legov.d	$⊢ φ \to D \in P$
Assertion	legov	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \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		legov.a	$⊢ φ \to A \in P$
7		legov.b	$⊢ φ \to B \in P$
8		legov.c	$⊢ φ \to C \in P$
9		legov.d	$⊢ φ \to D \in P$
10	1 2 3 4 5	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))\}$
11	10	breqd	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow (A \underset{˙}{-} B) \{⟨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))\} (C \underset{˙}{-} D))$
12		ovex	$⊢ A \underset{˙}{-} B \in V$
13		ovex	$⊢ C \underset{˙}{-} D \in V$
14		simpr	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to f = C \underset{˙}{-} D$
15	14	eqeq1d	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to (f = x \underset{˙}{-} y \leftrightarrow C \underset{˙}{-} D = x \underset{˙}{-} y)$
16		simpl	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to e = A \underset{˙}{-} B$
17	16	eqeq1d	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to (e = x \underset{˙}{-} z \leftrightarrow A \underset{˙}{-} B = x \underset{˙}{-} z)$
18	17	anbi2d	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to ((z \in (x I y) \land e = x \underset{˙}{-} z) \leftrightarrow (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
19	18	rexbidv	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \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 A \underset{˙}{-} B = x \underset{˙}{-} z))$
20	15 19	anbi12d	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \to ((f = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land e = x \underset{˙}{-} z)) \leftrightarrow (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)))$
21	20	2rexbidv	$⊢ (e = A \underset{˙}{-} B \land f = C \underset{˙}{-} D) \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 (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)))$
22		eqid	$⊢ \{⟨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))\} = \{⟨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))\}$
23	12 13 21 22	braba	$⊢ (A \underset{˙}{-} B) \{⟨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))\} (C \underset{˙}{-} D) \leftrightarrow \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
24	11 23	bitrdi	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)))$
25		anass	$⊢ ((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)) \leftrightarrow (((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)))$
26	25	anbi1i	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)) \land x \in P) \leftrightarrow ((((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \land x \in P)$
27		eqid	$⊢ \sim_{𝒢} (G) = \sim_{𝒢} (G)$
28	5	ad5antr	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to G \in 𝒢_{Tarski}$
29	28	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to G \in 𝒢_{Tarski}$
30		simp-5r	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to c \in P$
31	30	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to c \in P$
32		simpllr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to x \in P$
33		simp-4r	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to d \in P$
34	33	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to d \in P$
35	8	ad5antr	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to C \in P$
36	35	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to C \in P$
37		simprl	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to z \in P$
38	9	ad5antr	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to D \in P$
39	38	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to D \in P$
40		simprr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩$
41	1 2 3 27 29 31 34 32 36 39 37 40	cgr3swap23	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to ⟨“ c x d ”⟩ \sim_{𝒢} (G) ⟨“ C z D ”⟩$
42		simprl	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to x \in (c I d)$
43	42	adantr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to x \in (c I d)$
44	1 2 3 27 29 31 32 34 36 37 39 41 43	tgbtwnxfr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to z \in (C I D)$
45		simplrr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to A \underset{˙}{-} B = c \underset{˙}{-} x$
46	1 2 3 27 29 31 32 34 36 37 39 41	cgr3simp1	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to c \underset{˙}{-} x = C \underset{˙}{-} z$
47	45 46	eqtrd	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to A \underset{˙}{-} B = C \underset{˙}{-} z$
48	44 47	jca	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \land (z \in P \land ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩)) \to (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
49		eqid	$⊢ {Line}_{𝒢} (G) = {Line}_{𝒢} (G)$
50		simplr	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to x \in P$
51	1 49 3 28 30 50 33 42	btwncolg3	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to (d \in (c {Line}_{𝒢} (G) x) \lor c = x)$
52		simpllr	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to C \underset{˙}{-} D = c \underset{˙}{-} d$
53	52	eqcomd	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to c \underset{˙}{-} d = C \underset{˙}{-} D$
54	1 49 3 28 30 33 50 27 35 38 2 51 53	lnext	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to \exists z \in P ⟨“ c d x ”⟩ \sim_{𝒢} (G) ⟨“ C D z ”⟩$
55	48 54	reximddv	$⊢ (((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
56	55	adantllr	$⊢ ((((((φ \land c \in P) \land d \in P) \land C \underset{˙}{-} D = c \underset{˙}{-} d) \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
57	26 56	sylanbr	$⊢ (((((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \land x \in P) \land (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
58		simprr	$⊢ (((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \to \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)$
59		eleq1w	$⊢ x = z \to (x \in (c I d) \leftrightarrow z \in (c I d))$
60		oveq2	$⊢ x = z \to c \underset{˙}{-} x = c \underset{˙}{-} z$
61	60	eqeq2d	$⊢ x = z \to (A \underset{˙}{-} B = c \underset{˙}{-} x \leftrightarrow A \underset{˙}{-} B = c \underset{˙}{-} z)$
62	59 61	anbi12d	$⊢ x = z \to ((x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x) \leftrightarrow (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))$
63	62	cbvrexvw	$⊢ \exists x \in P (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x) \leftrightarrow \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)$
64	58 63	sylibr	$⊢ (((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \to \exists x \in P (x \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} x)$
65	57 64	r19.29a	$⊢ (((φ \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
66	65	adantl3r	$⊢ ((((φ \land \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))) \land c \in P) \land d \in P) \land (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
67		simpr	$⊢ (φ \land \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))) \to \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
68		oveq1	$⊢ c = x \to c \underset{˙}{-} d = x \underset{˙}{-} d$
69	68	eqeq2d	$⊢ c = x \to (C \underset{˙}{-} D = c \underset{˙}{-} d \leftrightarrow C \underset{˙}{-} D = x \underset{˙}{-} d)$
70		oveq1	$⊢ c = x \to c I d = x I d$
71	70	eleq2d	$⊢ c = x \to (z \in (c I d) \leftrightarrow z \in (x I d))$
72		oveq1	$⊢ c = x \to c \underset{˙}{-} z = x \underset{˙}{-} z$
73	72	eqeq2d	$⊢ c = x \to (A \underset{˙}{-} B = c \underset{˙}{-} z \leftrightarrow A \underset{˙}{-} B = x \underset{˙}{-} z)$
74	71 73	anbi12d	$⊢ c = x \to ((z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z) \leftrightarrow (z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
75	74	rexbidv	$⊢ c = x \to (\exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z) \leftrightarrow \exists z \in P (z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
76	69 75	anbi12d	$⊢ c = x \to ((C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)) \leftrightarrow (C \underset{˙}{-} D = x \underset{˙}{-} d \land \exists z \in P (z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z)))$
77		oveq2	$⊢ d = y \to x \underset{˙}{-} d = x \underset{˙}{-} y$
78	77	eqeq2d	$⊢ d = y \to (C \underset{˙}{-} D = x \underset{˙}{-} d \leftrightarrow C \underset{˙}{-} D = x \underset{˙}{-} y)$
79		oveq2	$⊢ d = y \to x I d = x I y$
80	79	eleq2d	$⊢ d = y \to (z \in (x I d) \leftrightarrow z \in (x I y))$
81	80	anbi1d	$⊢ d = y \to ((z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z) \leftrightarrow (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
82	81	rexbidv	$⊢ d = y \to (\exists z \in P (z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z) \leftrightarrow \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
83	78 82	anbi12d	$⊢ d = y \to ((C \underset{˙}{-} D = x \underset{˙}{-} d \land \exists z \in P (z \in (x I d) \land A \underset{˙}{-} B = x \underset{˙}{-} z)) \leftrightarrow (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)))$
84	76 83	cbvrex2vw	$⊢ \exists c \in P \exists d \in P (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z)) \leftrightarrow \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
85	67 84	sylibr	$⊢ (φ \land \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))) \to \exists c \in P \exists d \in P (C \underset{˙}{-} D = c \underset{˙}{-} d \land \exists z \in P (z \in (c I d) \land A \underset{˙}{-} B = c \underset{˙}{-} z))$
86	66 85	r19.29vva	$⊢ (φ \land \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
87	8	adantr	$⊢ (φ \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to C \in P$
88	9	adantr	$⊢ (φ \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to D \in P$
89		eqidd	$⊢ (φ \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to C \underset{˙}{-} D = C \underset{˙}{-} D$
90		simpr	$⊢ (φ \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)$
91		oveq1	$⊢ x = C \to x \underset{˙}{-} y = C \underset{˙}{-} y$
92	91	eqeq2d	$⊢ x = C \to (C \underset{˙}{-} D = x \underset{˙}{-} y \leftrightarrow C \underset{˙}{-} D = C \underset{˙}{-} y)$
93		oveq1	$⊢ x = C \to x I y = C I y$
94	93	eleq2d	$⊢ x = C \to (z \in (x I y) \leftrightarrow z \in (C I y))$
95		oveq1	$⊢ x = C \to x \underset{˙}{-} z = C \underset{˙}{-} z$
96	95	eqeq2d	$⊢ x = C \to (A \underset{˙}{-} B = x \underset{˙}{-} z \leftrightarrow A \underset{˙}{-} B = C \underset{˙}{-} z)$
97	94 96	anbi12d	$⊢ x = C \to ((z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z) \leftrightarrow (z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
98	97	rexbidv	$⊢ x = C \to (\exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z) \leftrightarrow \exists z \in P (z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
99	92 98	anbi12d	$⊢ x = C \to ((C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)) \leftrightarrow (C \underset{˙}{-} D = C \underset{˙}{-} y \land \exists z \in P (z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z)))$
100		oveq2	$⊢ y = D \to C \underset{˙}{-} y = C \underset{˙}{-} D$
101	100	eqeq2d	$⊢ y = D \to (C \underset{˙}{-} D = C \underset{˙}{-} y \leftrightarrow C \underset{˙}{-} D = C \underset{˙}{-} D)$
102		oveq2	$⊢ y = D \to C I y = C I D$
103	102	eleq2d	$⊢ y = D \to (z \in (C I y) \leftrightarrow z \in (C I D))$
104	103	anbi1d	$⊢ y = D \to ((z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z) \leftrightarrow (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
105	104	rexbidv	$⊢ y = D \to (\exists z \in P (z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z) \leftrightarrow \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
106	101 105	anbi12d	$⊢ y = D \to ((C \underset{˙}{-} D = C \underset{˙}{-} y \land \exists z \in P (z \in (C I y) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \leftrightarrow (C \underset{˙}{-} D = C \underset{˙}{-} D \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)))$
107	99 106	rspc2ev	$⊢ (C \in P \land D \in P \land (C \underset{˙}{-} D = C \underset{˙}{-} D \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))) \to \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
108	87 88 89 90 107	syl112anc	$⊢ (φ \land \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z)) \to \exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z))$
109	86 108	impbida	$⊢ φ \to (\exists x \in P \exists y \in P (C \underset{˙}{-} D = x \underset{˙}{-} y \land \exists z \in P (z \in (x I y) \land A \underset{˙}{-} B = x \underset{˙}{-} z)) \leftrightarrow \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$
110	24 109	bitrd	$⊢ φ \to ((A \underset{˙}{-} B) \underset{˙}{\leq} (C \underset{˙}{-} D) \leftrightarrow \exists z \in P (z \in (C I D) \land A \underset{˙}{-} B = C \underset{˙}{-} z))$

Metamath Proof Explorer

Theorem legov

Proof