br8d

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013) (Revised by Mario Carneiro, 3-May-2015) (Revised by Thierry Arnoux, 21-Mar-2019)

	Ref	Expression
Hypotheses	br8d.1	$⊢ a = A \to (ψ \leftrightarrow χ)$
	br8d.2	$⊢ b = B \to (χ \leftrightarrow θ)$
	br8d.3	$⊢ c = C \to (θ \leftrightarrow τ)$
	br8d.4	$⊢ d = D \to (τ \leftrightarrow η)$
	br8d.5	$⊢ e = E \to (η \leftrightarrow ζ)$
	br8d.6	$⊢ f = F \to (ζ \leftrightarrow σ)$
	br8d.7	$⊢ g = G \to (σ \leftrightarrow ρ)$
	br8d.8	$⊢ h = H \to (ρ \leftrightarrow μ)$
	br8d.10	$⊢ φ \to R = \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\}$
	br8d.11	$⊢ φ \to A \in P$
	br8d.12	$⊢ φ \to B \in P$
	br8d.13	$⊢ φ \to C \in P$
	br8d.14	$⊢ φ \to D \in P$
	br8d.15	$⊢ φ \to E \in P$
	br8d.16	$⊢ φ \to F \in P$
	br8d.17	$⊢ φ \to G \in P$
	br8d.18	$⊢ φ \to H \in P$
Assertion	br8d	$⊢ φ \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow μ)$

Proof

Step	Hyp	Ref	Expression
1		br8d.1	$⊢ a = A \to (ψ \leftrightarrow χ)$
2		br8d.2	$⊢ b = B \to (χ \leftrightarrow θ)$
3		br8d.3	$⊢ c = C \to (θ \leftrightarrow τ)$
4		br8d.4	$⊢ d = D \to (τ \leftrightarrow η)$
5		br8d.5	$⊢ e = E \to (η \leftrightarrow ζ)$
6		br8d.6	$⊢ f = F \to (ζ \leftrightarrow σ)$
7		br8d.7	$⊢ g = G \to (σ \leftrightarrow ρ)$
8		br8d.8	$⊢ h = H \to (ρ \leftrightarrow μ)$
9		br8d.10	$⊢ φ \to R = \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\}$
10		br8d.11	$⊢ φ \to A \in P$
11		br8d.12	$⊢ φ \to B \in P$
12		br8d.13	$⊢ φ \to C \in P$
13		br8d.14	$⊢ φ \to D \in P$
14		br8d.15	$⊢ φ \to E \in P$
15		br8d.16	$⊢ φ \to F \in P$
16		br8d.17	$⊢ φ \to G \in P$
17		br8d.18	$⊢ φ \to H \in P$
18	9	breqd	$⊢ φ \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\} ⟨⟨E, F⟩, ⟨G, H⟩⟩)$
19		opex	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ \in V$
20		opex	$⊢ ⟨⟨E, F⟩, ⟨G, H⟩⟩ \in V$
21		eqeq1	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩)$
22	21	3anbi1d	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to ((p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
23	22	rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
24	23	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
25	24	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
26	25	2rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
27	26	rexbidv	$⊢ p = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
28		eqeq1	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩)$
29	28	3anbi2d	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
30	29	rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
31	30	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
32	31	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
33	32	2rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
34	33	rexbidv	$⊢ q = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
35		eqid	$⊢ \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\} = \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\}$
36	19 20 27 34 35	brab	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ \{⟨p, q⟩ \| \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (p = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land q = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)\} ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)$
37	18 36	syl6bb	$⊢ φ \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
38		opex	$⊢ ⟨a, b⟩ \in V$
39		opex	$⊢ ⟨c, d⟩ \in V$
40	38 39	opth	$⊢ ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \leftrightarrow (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩)$
41		vex	$⊢ a \in V$
42		vex	$⊢ b \in V$
43	41 42	opth	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \leftrightarrow (a = A \land b = B)$
44	1 2	sylan9bb	$⊢ (a = A \land b = B) \to (ψ \leftrightarrow θ)$
45	43 44	sylbi	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \to (ψ \leftrightarrow θ)$
46		vex	$⊢ c \in V$
47		vex	$⊢ d \in V$
48	46 47	opth	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \leftrightarrow (c = C \land d = D)$
49	3 4	sylan9bb	$⊢ (c = C \land d = D) \to (θ \leftrightarrow η)$
50	48 49	sylbi	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \to (θ \leftrightarrow η)$
51	45 50	sylan9bb	$⊢ (⟨a, b⟩ = ⟨A, B⟩ \land ⟨c, d⟩ = ⟨C, D⟩) \to (ψ \leftrightarrow η)$
52	40 51	sylbi	$⊢ ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \to (ψ \leftrightarrow η)$
53	52	eqcoms	$⊢ ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \to (ψ \leftrightarrow η)$
54		opex	$⊢ ⟨e, f⟩ \in V$
55		opex	$⊢ ⟨g, h⟩ \in V$
56	54 55	opth	$⊢ ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow (⟨e, f⟩ = ⟨E, F⟩ \land ⟨g, h⟩ = ⟨G, H⟩)$
57		vex	$⊢ e \in V$
58		vex	$⊢ f \in V$
59	57 58	opth	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \leftrightarrow (e = E \land f = F)$
60	5 6	sylan9bb	$⊢ (e = E \land f = F) \to (η \leftrightarrow σ)$
61	59 60	sylbi	$⊢ ⟨e, f⟩ = ⟨E, F⟩ \to (η \leftrightarrow σ)$
62		vex	$⊢ g \in V$
63		vex	$⊢ h \in V$
64	62 63	opth	$⊢ ⟨g, h⟩ = ⟨G, H⟩ \leftrightarrow (g = G \land h = H)$
65	7 8	sylan9bb	$⊢ (g = G \land h = H) \to (σ \leftrightarrow μ)$
66	64 65	sylbi	$⊢ ⟨g, h⟩ = ⟨G, H⟩ \to (σ \leftrightarrow μ)$
67	61 66	sylan9bb	$⊢ (⟨e, f⟩ = ⟨E, F⟩ \land ⟨g, h⟩ = ⟨G, H⟩) \to (η \leftrightarrow μ)$
68	56 67	sylbi	$⊢ ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \to (η \leftrightarrow μ)$
69	68	eqcoms	$⊢ ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \to (η \leftrightarrow μ)$
70	53 69	sylan9bb	$⊢ (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩) \to (ψ \leftrightarrow μ)$
71	70	biimp3a	$⊢ (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ$
72	71	a1i	$⊢ (((((((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land a \in P) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \land (f \in P \land g \in P)) \land h \in P) \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
73	72	rexlimdva	$⊢ ((((((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land a \in P) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \land (f \in P \land g \in P)) \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
74	73	rexlimdvva	$⊢ (((((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land a \in P) \land (b \in P \land c \in P)) \land (d \in P \land e \in P)) \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
75	74	rexlimdvva	$⊢ ((((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land a \in P) \land (b \in P \land c \in P)) \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
76	75	rexlimdvva	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land a \in P) \to (\exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
77	76	rexlimdva	$⊢ ((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \to μ)$
78		simpl1l	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to A \in P$
79		simpl1r	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to B \in P$
80		simpl21	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to C \in P$
81		simpl22	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to D \in P$
82		simpl23	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to E \in P$
83		simpl31	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to F \in P$
84		simpl32	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to G \in P$
85		simpl33	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to H \in P$
86		eqidd	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩$
87		eqidd	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩$
88		simpr	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to μ$
89		opeq1	$⊢ g = G \to ⟨g, h⟩ = ⟨G, h⟩$
90	89	opeq2d	$⊢ g = G \to ⟨⟨E, F⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩$
91	90	eqeq2d	$⊢ g = G \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩)$
92	91 7	3anbi23d	$⊢ g = G \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \land ρ))$
93		opeq2	$⊢ h = H \to ⟨G, h⟩ = ⟨G, H⟩$
94	93	opeq2d	$⊢ h = H \to ⟨⟨E, F⟩, ⟨G, h⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩$
95	94	eqeq2d	$⊢ h = H \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩)$
96	95 8	3anbi23d	$⊢ h = H \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, h⟩⟩ \land ρ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land μ))$
97	92 96	rspc2ev	$⊢ (G \in P \land H \in P \land (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨G, H⟩⟩ \land μ)) \to \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ)$
98	84 85 86 87 88 97	syl113anc	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ)$
99		opeq2	$⊢ d = D \to ⟨C, d⟩ = ⟨C, D⟩$
100	99	opeq2d	$⊢ d = D \to ⟨⟨A, B⟩, ⟨C, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩$
101	100	eqeq2d	$⊢ d = D \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩)$
102	101 4	3anbi13d	$⊢ d = D \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land η))$
103	102	2rexbidv	$⊢ d = D \to (\exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ) \leftrightarrow \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land η))$
104		opeq1	$⊢ e = E \to ⟨e, f⟩ = ⟨E, f⟩$
105	104	opeq1d	$⊢ e = E \to ⟨⟨e, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩$
106	105	eqeq2d	$⊢ e = E \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩)$
107	106 5	3anbi23d	$⊢ e = E \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land η) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land ζ))$
108	107	2rexbidv	$⊢ e = E \to (\exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land η) \leftrightarrow \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land ζ))$
109		opeq2	$⊢ f = F \to ⟨E, f⟩ = ⟨E, F⟩$
110	109	opeq1d	$⊢ f = F \to ⟨⟨E, f⟩, ⟨g, h⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩$
111	110	eqeq2d	$⊢ f = F \to (⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \leftrightarrow ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩)$
112	111 6	3anbi23d	$⊢ f = F \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land ζ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ))$
113	112	2rexbidv	$⊢ f = F \to (\exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, f⟩, ⟨g, h⟩⟩ \land ζ) \leftrightarrow \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ))$
114	103 108 113	rspc3ev	$⊢ ((D \in P \land E \in P \land F \in P) \land \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, D⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨E, F⟩, ⟨g, h⟩⟩ \land σ)) \to \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ)$
115	81 82 83 98 114	syl31anc	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ)$
116		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
117	116	opeq1d	$⊢ a = A \to ⟨⟨a, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩$
118	117	eqeq2d	$⊢ a = A \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩)$
119	118 1	3anbi13d	$⊢ a = A \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
120	119	rexbidv	$⊢ a = A \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
121	120	2rexbidv	$⊢ a = A \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
122	121	2rexbidv	$⊢ a = A \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ))$
123		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
124	123	opeq1d	$⊢ b = B \to ⟨⟨A, b⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩$
125	124	eqeq2d	$⊢ b = B \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩)$
126	125 2	3anbi13d	$⊢ b = B \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
127	126	rexbidv	$⊢ b = B \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
128	127	2rexbidv	$⊢ b = B \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
129	128	2rexbidv	$⊢ b = B \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land χ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ))$
130		opeq1	$⊢ c = C \to ⟨c, d⟩ = ⟨C, d⟩$
131	130	opeq2d	$⊢ c = C \to ⟨⟨A, B⟩, ⟨c, d⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩$
132	131	eqeq2d	$⊢ c = C \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \leftrightarrow ⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩)$
133	132 3	3anbi13d	$⊢ c = C \to ((⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
134	133	rexbidv	$⊢ c = C \to (\exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
135	134	2rexbidv	$⊢ c = C \to (\exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
136	135	2rexbidv	$⊢ c = C \to (\exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land θ) \leftrightarrow \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ))$
137	122 129 136	rspc3ev	$⊢ ((A \in P \land B \in P \land C \in P) \land \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨A, B⟩, ⟨C, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land τ)) \to \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)$
138	78 79 80 115 137	syl31anc	$⊢ (((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \land μ) \to \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ)$
139	138	ex	$⊢ ((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \to (μ \to \exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ))$
140	77 139	impbid	$⊢ ((A \in P \land B \in P) \land (C \in P \land D \in P \land E \in P) \land (F \in P \land G \in P \land H \in P)) \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow μ)$
141	10 11 12 13 14 15 16 17 140	syl233anc	$⊢ φ \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P \exists e \in P \exists f \in P \exists g \in P \exists h \in P (⟨⟨A, B⟩, ⟨C, D⟩⟩ = ⟨⟨a, b⟩, ⟨c, d⟩⟩ \land ⟨⟨E, F⟩, ⟨G, H⟩⟩ = ⟨⟨e, f⟩, ⟨g, h⟩⟩ \land ψ) \leftrightarrow μ)$
142	37 141	bitrd	$⊢ φ \to (⟨⟨A, B⟩, ⟨C, D⟩⟩ R ⟨⟨E, F⟩, ⟨G, H⟩⟩ \leftrightarrow μ)$

Metamath Proof Explorer

Theorem br8d

Proof