axtg5seg

Description: Five segments axiom, Axiom A5 of Schwabhauser p. 11. Take two triangles X Z U and A C V , a point Y on X Z , and a point B on A C . If all corresponding line segments except for Z U and C V are congruent ( i.e., X Y .A B , Y Z .B C , X U .A V , and Y U .B V ), then Z U and C V are also congruent. As noted in Axiom 5 of Tarski1999 p. 178, "this axiom is similar in character to the well-known theorems of Euclidean geometry that allow one to conclude, from hypotheses about the congruence of certain corresponding sides and angles in two triangles, the congruence of other corresponding sides and angles." (Contributed by Thierry Arnoux, 14-Mar-2019)

	Ref	Expression
Hypotheses	axtrkg.p	$⊢ P = {Base}_{G}$
	axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
	axtrkg.i	$⊢ I = Itv (G)$
	axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
	axtg5seg.1	$⊢ φ \to X \in P$
	axtg5seg.2	$⊢ φ \to Y \in P$
	axtg5seg.3	$⊢ φ \to Z \in P$
	axtg5seg.4	$⊢ φ \to A \in P$
	axtg5seg.5	$⊢ φ \to B \in P$
	axtg5seg.6	$⊢ φ \to C \in P$
	axtg5seg.7	$⊢ φ \to U \in P$
	axtg5seg.8	$⊢ φ \to V \in P$
	axtg5seg.9	$⊢ φ \to X \neq Y$
	axtg5seg.10	$⊢ φ \to Y \in (X I Z)$
	axtg5seg.11	$⊢ φ \to B \in (A I C)$
	axtg5seg.12	$⊢ φ \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
	axtg5seg.13	$⊢ φ \to Y \underset{˙}{-} Z = B \underset{˙}{-} C$
	axtg5seg.14	$⊢ φ \to X \underset{˙}{-} U = A \underset{˙}{-} V$
	axtg5seg.15	$⊢ φ \to Y \underset{˙}{-} U = B \underset{˙}{-} V$
Assertion	axtg5seg	$⊢ φ \to Z \underset{˙}{-} U = C \underset{˙}{-} V$

Proof

Step	Hyp	Ref	Expression
1		axtrkg.p	$⊢ P = {Base}_{G}$
2		axtrkg.d	$⊢ \underset{˙}{-} = dist (G)$
3		axtrkg.i	$⊢ I = Itv (G)$
4		axtrkg.g	$⊢ φ \to G \in 𝒢_{Tarski}$
5		axtg5seg.1	$⊢ φ \to X \in P$
6		axtg5seg.2	$⊢ φ \to Y \in P$
7		axtg5seg.3	$⊢ φ \to Z \in P$
8		axtg5seg.4	$⊢ φ \to A \in P$
9		axtg5seg.5	$⊢ φ \to B \in P$
10		axtg5seg.6	$⊢ φ \to C \in P$
11		axtg5seg.7	$⊢ φ \to U \in P$
12		axtg5seg.8	$⊢ φ \to V \in P$
13		axtg5seg.9	$⊢ φ \to X \neq Y$
14		axtg5seg.10	$⊢ φ \to Y \in (X I Z)$
15		axtg5seg.11	$⊢ φ \to B \in (A I C)$
16		axtg5seg.12	$⊢ φ \to X \underset{˙}{-} Y = A \underset{˙}{-} B$
17		axtg5seg.13	$⊢ φ \to Y \underset{˙}{-} Z = B \underset{˙}{-} C$
18		axtg5seg.14	$⊢ φ \to X \underset{˙}{-} U = A \underset{˙}{-} V$
19		axtg5seg.15	$⊢ φ \to Y \underset{˙}{-} U = B \underset{˙}{-} V$
20		df-trkg	$⊢ 𝒢_{Tarski} = (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\})$
21		inss2	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}$
22		inss1	$⊢ 𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\} \subseteq 𝒢_{Tarski}^{CB}$
23	21 22	sstri	$⊢ (𝒢_{Tarski}^{C} \cap 𝒢_{Tarski}^{B}) \cap (𝒢_{Tarski}^{CB} \cap \{f \| \underset{˙}{[} {Base}_{f} / p \underset{˙}{]} \underset{˙}{[} Itv (f) / i \underset{˙}{]} {Line}_{𝒢} (f) = (x \in p, y \in (p ∖ \{x\}) ⟼ \{z \in p \| (z \in (x i y) \lor x \in (z i y) \lor y \in (x i z))\})\}) \subseteq 𝒢_{Tarski}^{CB}$
24	20 23	eqsstri	$⊢ 𝒢_{Tarski} \subseteq 𝒢_{Tarski}^{CB}$
25	24 4	sselid	$⊢ φ \to G \in 𝒢_{Tarski}^{CB}$
26	1 2 3	istrkgcb	$⊢ G \in 𝒢_{Tarski}^{CB} \leftrightarrow (G \in V \land (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \land \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b)))$
27	26	simprbi	$⊢ G \in 𝒢_{Tarski}^{CB} \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \land \forall x \in P \forall y \in P \forall a \in P \forall b \in P \exists z \in P (y \in (x I z) \land y \underset{˙}{-} z = a \underset{˙}{-} b))$
28	27	simpld	$⊢ G \in 𝒢_{Tarski}^{CB} \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v)$
29	25 28	syl	$⊢ φ \to \forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v)$
30		neeq1	$⊢ x = X \to (x \neq y \leftrightarrow X \neq y)$
31		oveq1	$⊢ x = X \to x I z = X I z$
32	31	eleq2d	$⊢ x = X \to (y \in (x I z) \leftrightarrow y \in (X I z))$
33	30 32	3anbi12d	$⊢ x = X \to ((x \neq y \land y \in (x I z) \land b \in (a I c)) \leftrightarrow (X \neq y \land y \in (X I z) \land b \in (a I c)))$
34		oveq1	$⊢ x = X \to x \underset{˙}{-} y = X \underset{˙}{-} y$
35	34	eqeq1d	$⊢ x = X \to (x \underset{˙}{-} y = a \underset{˙}{-} b \leftrightarrow X \underset{˙}{-} y = a \underset{˙}{-} b)$
36	35	anbi1d	$⊢ x = X \to ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c))$
37		oveq1	$⊢ x = X \to x \underset{˙}{-} u = X \underset{˙}{-} u$
38	37	eqeq1d	$⊢ x = X \to (x \underset{˙}{-} u = a \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} u = a \underset{˙}{-} v)$
39	38	anbi1d	$⊢ x = X \to ((x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))$
40	36 39	anbi12d	$⊢ x = X \to (((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v)))$
41	33 40	anbi12d	$⊢ x = X \to (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \leftrightarrow ((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))))$
42	41	imbi1d	$⊢ x = X \to ((((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
43	42	ralbidv	$⊢ x = X \to (\forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
44	43	2ralbidv	$⊢ x = X \to (\forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall b \in P \forall c \in P \forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
45	44	2ralbidv	$⊢ x = X \to (\forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
46		neeq2	$⊢ y = Y \to (X \neq y \leftrightarrow X \neq Y)$
47		eleq1	$⊢ y = Y \to (y \in (X I z) \leftrightarrow Y \in (X I z))$
48	46 47	3anbi12d	$⊢ y = Y \to ((X \neq y \land y \in (X I z) \land b \in (a I c)) \leftrightarrow (X \neq Y \land Y \in (X I z) \land b \in (a I c)))$
49		oveq2	$⊢ y = Y \to X \underset{˙}{-} y = X \underset{˙}{-} Y$
50	49	eqeq1d	$⊢ y = Y \to (X \underset{˙}{-} y = a \underset{˙}{-} b \leftrightarrow X \underset{˙}{-} Y = a \underset{˙}{-} b)$
51		oveq1	$⊢ y = Y \to y \underset{˙}{-} z = Y \underset{˙}{-} z$
52	51	eqeq1d	$⊢ y = Y \to (y \underset{˙}{-} z = b \underset{˙}{-} c \leftrightarrow Y \underset{˙}{-} z = b \underset{˙}{-} c)$
53	50 52	anbi12d	$⊢ y = Y \to ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c))$
54		oveq1	$⊢ y = Y \to y \underset{˙}{-} u = Y \underset{˙}{-} u$
55	54	eqeq1d	$⊢ y = Y \to (y \underset{˙}{-} u = b \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} u = b \underset{˙}{-} v)$
56	55	anbi2d	$⊢ y = Y \to ((X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))$
57	53 56	anbi12d	$⊢ y = Y \to (((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v)))$
58	48 57	anbi12d	$⊢ y = Y \to (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))))$
59	58	imbi1d	$⊢ y = Y \to ((((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
60	59	ralbidv	$⊢ y = Y \to (\forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
61	60	2ralbidv	$⊢ y = Y \to (\forall b \in P \forall c \in P \forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
62	61	2ralbidv	$⊢ y = Y \to (\forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq y \land y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v))$
63		oveq2	$⊢ z = Z \to X I z = X I Z$
64	63	eleq2d	$⊢ z = Z \to (Y \in (X I z) \leftrightarrow Y \in (X I Z))$
65	64	3anbi2d	$⊢ z = Z \to ((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \leftrightarrow (X \neq Y \land Y \in (X I Z) \land b \in (a I c)))$
66		oveq2	$⊢ z = Z \to Y \underset{˙}{-} z = Y \underset{˙}{-} Z$
67	66	eqeq1d	$⊢ z = Z \to (Y \underset{˙}{-} z = b \underset{˙}{-} c \leftrightarrow Y \underset{˙}{-} Z = b \underset{˙}{-} c)$
68	67	anbi2d	$⊢ z = Z \to ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c))$
69	68	anbi1d	$⊢ z = Z \to (((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v)))$
70	65 69	anbi12d	$⊢ z = Z \to (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))))$
71		oveq1	$⊢ z = Z \to z \underset{˙}{-} u = Z \underset{˙}{-} u$
72	71	eqeq1d	$⊢ z = Z \to (z \underset{˙}{-} u = c \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} u = c \underset{˙}{-} v)$
73	70 72	imbi12d	$⊢ z = Z \to ((((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
74	73	ralbidv	$⊢ z = Z \to (\forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
75	74	2ralbidv	$⊢ z = Z \to (\forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
76	75	2ralbidv	$⊢ z = Z \to (\forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
77	45 62 76	rspc3v	$⊢ (X \in P \land Y \in P \land Z \in P) \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \to \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
78	5 6 7 77	syl3anc	$⊢ φ \to (\forall x \in P \forall y \in P \forall z \in P \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((x \neq y \land y \in (x I z) \land b \in (a I c)) \land ((x \underset{˙}{-} y = a \underset{˙}{-} b \land y \underset{˙}{-} z = b \underset{˙}{-} c) \land (x \underset{˙}{-} u = a \underset{˙}{-} v \land y \underset{˙}{-} u = b \underset{˙}{-} v))) \to z \underset{˙}{-} u = c \underset{˙}{-} v) \to \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v))$
79	29 78	mpd	$⊢ φ \to \forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v)$
80		oveq2	$⊢ u = U \to X \underset{˙}{-} u = X \underset{˙}{-} U$
81	80	eqeq1d	$⊢ u = U \to (X \underset{˙}{-} u = a \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} U = a \underset{˙}{-} v)$
82		oveq2	$⊢ u = U \to Y \underset{˙}{-} u = Y \underset{˙}{-} U$
83	82	eqeq1d	$⊢ u = U \to (Y \underset{˙}{-} u = b \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} U = b \underset{˙}{-} v)$
84	81 83	anbi12d	$⊢ u = U \to ((X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))$
85	84	anbi2d	$⊢ u = U \to (((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v)))$
86	85	anbi2d	$⊢ u = U \to (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))))$
87		oveq2	$⊢ u = U \to Z \underset{˙}{-} u = Z \underset{˙}{-} U$
88	87	eqeq1d	$⊢ u = U \to (Z \underset{˙}{-} u = c \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} U = c \underset{˙}{-} v)$
89	86 88	imbi12d	$⊢ u = U \to ((((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
90	89	2ralbidv	$⊢ u = U \to (\forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v) \leftrightarrow \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
91		oveq1	$⊢ a = A \to a I c = A I c$
92	91	eleq2d	$⊢ a = A \to (b \in (a I c) \leftrightarrow b \in (A I c))$
93	92	3anbi3d	$⊢ a = A \to ((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \leftrightarrow (X \neq Y \land Y \in (X I Z) \land b \in (A I c)))$
94		oveq1	$⊢ a = A \to a \underset{˙}{-} b = A \underset{˙}{-} b$
95	94	eqeq2d	$⊢ a = A \to (X \underset{˙}{-} Y = a \underset{˙}{-} b \leftrightarrow X \underset{˙}{-} Y = A \underset{˙}{-} b)$
96	95	anbi1d	$⊢ a = A \to ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c))$
97		oveq1	$⊢ a = A \to a \underset{˙}{-} v = A \underset{˙}{-} v$
98	97	eqeq2d	$⊢ a = A \to (X \underset{˙}{-} U = a \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} U = A \underset{˙}{-} v)$
99	98	anbi1d	$⊢ a = A \to ((X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))$
100	96 99	anbi12d	$⊢ a = A \to (((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v)))$
101	93 100	anbi12d	$⊢ a = A \to (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))))$
102	101	imbi1d	$⊢ a = A \to ((((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
103	102	2ralbidv	$⊢ a = A \to (\forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = a \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \leftrightarrow \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
104		eleq1	$⊢ b = B \to (b \in (A I c) \leftrightarrow B \in (A I c))$
105	104	3anbi3d	$⊢ b = B \to ((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \leftrightarrow (X \neq Y \land Y \in (X I Z) \land B \in (A I c)))$
106		oveq2	$⊢ b = B \to A \underset{˙}{-} b = A \underset{˙}{-} B$
107	106	eqeq2d	$⊢ b = B \to (X \underset{˙}{-} Y = A \underset{˙}{-} b \leftrightarrow X \underset{˙}{-} Y = A \underset{˙}{-} B)$
108		oveq1	$⊢ b = B \to b \underset{˙}{-} c = B \underset{˙}{-} c$
109	108	eqeq2d	$⊢ b = B \to (Y \underset{˙}{-} Z = b \underset{˙}{-} c \leftrightarrow Y \underset{˙}{-} Z = B \underset{˙}{-} c)$
110	107 109	anbi12d	$⊢ b = B \to ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c))$
111		oveq1	$⊢ b = B \to b \underset{˙}{-} v = B \underset{˙}{-} v$
112	111	eqeq2d	$⊢ b = B \to (Y \underset{˙}{-} U = b \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} U = B \underset{˙}{-} v)$
113	112	anbi2d	$⊢ b = B \to ((X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))$
114	110 113	anbi12d	$⊢ b = B \to (((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v)))$
115	105 114	anbi12d	$⊢ b = B \to (((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))))$
116	115	imbi1d	$⊢ b = B \to ((((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
117	116	2ralbidv	$⊢ b = B \to (\forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = b \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \leftrightarrow \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
118	90 103 117	rspc3v	$⊢ (U \in P \land A \in P \land B \in P) \to (\forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v) \to \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
119	11 8 9 118	syl3anc	$⊢ φ \to (\forall u \in P \forall a \in P \forall b \in P \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land b \in (a I c)) \land ((X \underset{˙}{-} Y = a \underset{˙}{-} b \land Y \underset{˙}{-} Z = b \underset{˙}{-} c) \land (X \underset{˙}{-} u = a \underset{˙}{-} v \land Y \underset{˙}{-} u = b \underset{˙}{-} v))) \to Z \underset{˙}{-} u = c \underset{˙}{-} v) \to \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v))$
120	79 119	mpd	$⊢ φ \to \forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v)$
121	13 14 15	3jca	$⊢ φ \to (X \neq Y \land Y \in (X I Z) \land B \in (A I C))$
122	16 17	jca	$⊢ φ \to (X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C)$
123	18 19	jca	$⊢ φ \to (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V)$
124	121 122 123	jca32	$⊢ φ \to ((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V)))$
125		oveq2	$⊢ c = C \to A I c = A I C$
126	125	eleq2d	$⊢ c = C \to (B \in (A I c) \leftrightarrow B \in (A I C))$
127	126	3anbi3d	$⊢ c = C \to ((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \leftrightarrow (X \neq Y \land Y \in (X I Z) \land B \in (A I C)))$
128		oveq2	$⊢ c = C \to B \underset{˙}{-} c = B \underset{˙}{-} C$
129	128	eqeq2d	$⊢ c = C \to (Y \underset{˙}{-} Z = B \underset{˙}{-} c \leftrightarrow Y \underset{˙}{-} Z = B \underset{˙}{-} C)$
130	129	anbi2d	$⊢ c = C \to ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \leftrightarrow (X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C))$
131	130	anbi1d	$⊢ c = C \to (((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v)))$
132	127 131	anbi12d	$⊢ c = C \to (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))))$
133		oveq1	$⊢ c = C \to c \underset{˙}{-} v = C \underset{˙}{-} v$
134	133	eqeq2d	$⊢ c = C \to (Z \underset{˙}{-} U = c \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} U = C \underset{˙}{-} v)$
135	132 134	imbi12d	$⊢ c = C \to ((((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = C \underset{˙}{-} v))$
136		oveq2	$⊢ v = V \to A \underset{˙}{-} v = A \underset{˙}{-} V$
137	136	eqeq2d	$⊢ v = V \to (X \underset{˙}{-} U = A \underset{˙}{-} v \leftrightarrow X \underset{˙}{-} U = A \underset{˙}{-} V)$
138		oveq2	$⊢ v = V \to B \underset{˙}{-} v = B \underset{˙}{-} V$
139	138	eqeq2d	$⊢ v = V \to (Y \underset{˙}{-} U = B \underset{˙}{-} v \leftrightarrow Y \underset{˙}{-} U = B \underset{˙}{-} V)$
140	137 139	anbi12d	$⊢ v = V \to ((X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v) \leftrightarrow (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V))$
141	140	anbi2d	$⊢ v = V \to (((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v)) \leftrightarrow ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V)))$
142	141	anbi2d	$⊢ v = V \to (((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \leftrightarrow ((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V))))$
143		oveq2	$⊢ v = V \to C \underset{˙}{-} v = C \underset{˙}{-} V$
144	143	eqeq2d	$⊢ v = V \to (Z \underset{˙}{-} U = C \underset{˙}{-} v \leftrightarrow Z \underset{˙}{-} U = C \underset{˙}{-} V)$
145	142 144	imbi12d	$⊢ v = V \to ((((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = C \underset{˙}{-} v) \leftrightarrow (((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V))) \to Z \underset{˙}{-} U = C \underset{˙}{-} V))$
146	135 145	rspc2v	$⊢ (C \in P \land V \in P) \to (\forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \to (((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V))) \to Z \underset{˙}{-} U = C \underset{˙}{-} V))$
147	10 12 146	syl2anc	$⊢ φ \to (\forall c \in P \forall v \in P (((X \neq Y \land Y \in (X I Z) \land B \in (A I c)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} c) \land (X \underset{˙}{-} U = A \underset{˙}{-} v \land Y \underset{˙}{-} U = B \underset{˙}{-} v))) \to Z \underset{˙}{-} U = c \underset{˙}{-} v) \to (((X \neq Y \land Y \in (X I Z) \land B \in (A I C)) \land ((X \underset{˙}{-} Y = A \underset{˙}{-} B \land Y \underset{˙}{-} Z = B \underset{˙}{-} C) \land (X \underset{˙}{-} U = A \underset{˙}{-} V \land Y \underset{˙}{-} U = B \underset{˙}{-} V))) \to Z \underset{˙}{-} U = C \underset{˙}{-} V))$
148	120 124 147	mp2d	$⊢ φ \to Z \underset{˙}{-} U = C \underset{˙}{-} V$

Metamath Proof Explorer

Theorem axtg5seg

Proof