br4

Description: Substitution for a four-place predicate. (Contributed by Scott Fenton, 9-Oct-2013) (Revised by Mario Carneiro, 14-Oct-2013)

	Ref	Expression
Hypotheses	br4.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
	br4.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
	br4.3	$⊢ c = C \to (χ \leftrightarrow θ)$
	br4.4	$⊢ d = D \to (θ \leftrightarrow τ)$
	br4.5	$⊢ x = X \to P = Q$
	br4.6	$⊢ R = \{⟨p, q⟩ \| \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ)\}$
Assertion	br4	$⊢ (X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \to (⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow τ)$

Proof

Step	Hyp	Ref	Expression
1		br4.1	$⊢ a = A \to (φ \leftrightarrow ψ)$
2		br4.2	$⊢ b = B \to (ψ \leftrightarrow χ)$
3		br4.3	$⊢ c = C \to (χ \leftrightarrow θ)$
4		br4.4	$⊢ d = D \to (θ \leftrightarrow τ)$
5		br4.5	$⊢ x = X \to P = Q$
6		br4.6	$⊢ R = \{⟨p, q⟩ \| \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ)\}$
7		opex	$⊢ ⟨A, B⟩ \in V$
8		opex	$⊢ ⟨C, D⟩ \in V$
9		eqeq1	$⊢ p = ⟨A, B⟩ \to (p = ⟨a, b⟩ \leftrightarrow ⟨A, B⟩ = ⟨a, b⟩)$
10	9	3anbi1d	$⊢ p = ⟨A, B⟩ \to ((p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ))$
11	10	rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists d \in P (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ))$
12	11	2rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists b \in P \exists c \in P \exists d \in P (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ))$
13	12	2rexbidv	$⊢ p = ⟨A, B⟩ \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (p = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ))$
14		eqeq1	$⊢ q = ⟨C, D⟩ \to (q = ⟨c, d⟩ \leftrightarrow ⟨C, D⟩ = ⟨c, d⟩)$
15	14	3anbi2d	$⊢ q = ⟨C, D⟩ \to ((⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
16	15	rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
17	16	2rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
18	17	2rexbidv	$⊢ q = ⟨C, D⟩ \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land q = ⟨c, d⟩ \land φ) \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
19	7 8 13 18 6	brab	$⊢ ⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)$
20		vex	$⊢ a \in V$
21		vex	$⊢ b \in V$
22	20 21	opth	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \leftrightarrow (a = A \land b = B)$
23	1 2	sylan9bb	$⊢ (a = A \land b = B) \to (φ \leftrightarrow χ)$
24	22 23	sylbi	$⊢ ⟨a, b⟩ = ⟨A, B⟩ \to (φ \leftrightarrow χ)$
25	24	eqcoms	$⊢ ⟨A, B⟩ = ⟨a, b⟩ \to (φ \leftrightarrow χ)$
26		vex	$⊢ c \in V$
27		vex	$⊢ d \in V$
28	26 27	opth	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \leftrightarrow (c = C \land d = D)$
29	3 4	sylan9bb	$⊢ (c = C \land d = D) \to (χ \leftrightarrow τ)$
30	28 29	sylbi	$⊢ ⟨c, d⟩ = ⟨C, D⟩ \to (χ \leftrightarrow τ)$
31	30	eqcoms	$⊢ ⟨C, D⟩ = ⟨c, d⟩ \to (χ \leftrightarrow τ)$
32	25 31	sylan9bb	$⊢ (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩) \to (φ \leftrightarrow τ)$
33	32	biimp3a	$⊢ (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \to τ$
34	33	a1i	$⊢ ((((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \land d \in P) \to ((⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \to τ)$
35	34	rexlimdva	$⊢ (((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land (x \in S \land a \in P)) \land (b \in P \land c \in P)) \to (\exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \to τ)$
36	35	rexlimdvva	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land (x \in S \land a \in P)) \to (\exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \to τ)$
37	36	rexlimdvva	$⊢ (X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \to τ)$
38		simpl1	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to X \in S$
39		simpl2l	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to A \in Q$
40		simpl2r	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to B \in Q$
41		simpl3l	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to C \in Q$
42		simpl3r	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to D \in Q$
43		eqidd	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to ⟨A, B⟩ = ⟨A, B⟩$
44		eqidd	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to ⟨C, D⟩ = ⟨C, D⟩$
45		simpr	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to τ$
46		opeq1	$⊢ c = C \to ⟨c, d⟩ = ⟨C, d⟩$
47	46	eqeq2d	$⊢ c = C \to (⟨C, D⟩ = ⟨c, d⟩ \leftrightarrow ⟨C, D⟩ = ⟨C, d⟩)$
48	47 3	3anbi23d	$⊢ c = C \to ((⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, d⟩ \land θ))$
49		opeq2	$⊢ d = D \to ⟨C, d⟩ = ⟨C, D⟩$
50	49	eqeq2d	$⊢ d = D \to (⟨C, D⟩ = ⟨C, d⟩ \leftrightarrow ⟨C, D⟩ = ⟨C, D⟩)$
51	50 4	3anbi23d	$⊢ d = D \to ((⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, d⟩ \land θ) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, D⟩ \land τ))$
52	48 51	rspc2ev	$⊢ (C \in Q \land D \in Q \land (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨C, D⟩ \land τ)) \to \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ)$
53	41 42 43 44 45 52	syl113anc	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ)$
54		opeq1	$⊢ a = A \to ⟨a, b⟩ = ⟨A, b⟩$
55	54	eqeq2d	$⊢ a = A \to (⟨A, B⟩ = ⟨a, b⟩ \leftrightarrow ⟨A, B⟩ = ⟨A, b⟩)$
56	55 1	3anbi13d	$⊢ a = A \to ((⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow (⟨A, B⟩ = ⟨A, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land ψ))$
57	56	2rexbidv	$⊢ a = A \to (\exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land ψ))$
58		opeq2	$⊢ b = B \to ⟨A, b⟩ = ⟨A, B⟩$
59	58	eqeq2d	$⊢ b = B \to (⟨A, B⟩ = ⟨A, b⟩ \leftrightarrow ⟨A, B⟩ = ⟨A, B⟩)$
60	59 2	3anbi13d	$⊢ b = B \to ((⟨A, B⟩ = ⟨A, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land ψ) \leftrightarrow (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ))$
61	60	2rexbidv	$⊢ b = B \to (\exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land ψ) \leftrightarrow \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ))$
62	57 61	rspc2ev	$⊢ (A \in Q \land B \in Q \land \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨A, B⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land χ)) \to \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)$
63	39 40 53 62	syl3anc	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)$
64	5	rexeqdv	$⊢ x = X \to (\exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
65	5 64	rexeqbidv	$⊢ x = X \to (\exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
66	5 65	rexeqbidv	$⊢ x = X \to (\exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow \exists b \in Q \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
67	5 66	rexeqbidv	$⊢ x = X \to (\exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
68	67	rspcev	$⊢ (X \in S \land \exists a \in Q \exists b \in Q \exists c \in Q \exists d \in Q (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)) \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)$
69	38 63 68	syl2anc	$⊢ ((X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \land τ) \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ)$
70	69	ex	$⊢ (X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \to (τ \to \exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ))$
71	37 70	impbid	$⊢ (X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \to (\exists x \in S \exists a \in P \exists b \in P \exists c \in P \exists d \in P (⟨A, B⟩ = ⟨a, b⟩ \land ⟨C, D⟩ = ⟨c, d⟩ \land φ) \leftrightarrow τ)$
72	19 71	bitrid	$⊢ (X \in S \land (A \in Q \land B \in Q) \land (C \in Q \land D \in Q)) \to (⟨A, B⟩ R ⟨C, D⟩ \leftrightarrow τ)$

Metamath Proof Explorer

Theorem br4

Proof