br4 - Mathbox for Scott Fenton

	Mathbox for Scott Fenton		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > br4		Structured version Visualization version GIF version

Theorem br4 33107

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

**Hypotheses**
Ref	Expression
br4.1	⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
br4.2	⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
br4.3	⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
br4.4	⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
br4.5	⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
br4.6	⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}

**Assertion**
Ref	Expression
br4	⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))

Distinct variable groups: 𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥,𝐴 𝐵,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜒,𝑏 𝑄,𝑎,𝑏,𝑐,𝑑,𝑥 𝐶,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝐷,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜓,𝑎 𝑋,𝑎,𝑏,𝑐,𝑑,𝑥 𝑃,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞 𝑆,𝑎,𝑏,𝑐,𝑑,𝑝,𝑞,𝑥 𝜏,𝑎,𝑏,𝑐,𝑑,𝑥 𝜃,𝑐 𝜑,𝑝,𝑞,𝑥 Allowed substitution hints: 𝜑(𝑎,𝑏,𝑐,𝑑) 𝜓(𝑥,𝑞,𝑝,𝑏,𝑐,𝑑) 𝜒(𝑥,𝑞,𝑝,𝑎,𝑐,𝑑) 𝜃(𝑥,𝑞,𝑝,𝑎,𝑏,𝑑) 𝜏(𝑞,𝑝) 𝑃(𝑥) 𝑄(𝑞,𝑝) 𝑅(𝑥,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝑋(𝑞,𝑝)

**Proof of Theorem br4**
Step	Hyp	Ref	Expression
1		opex 5321	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		opex 5321	. . 3 ⊢ ⟨𝐶, 𝐷⟩ ∈ V
3		eqeq1 2802	. . . . . . 7 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩))
4	3	3anbi1d 1437	. . . . . 6 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
5	4	rexbidv 3256	. . . . 5 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
6	5	2rexbidv 3259	. . . 4 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
7	6	2rexbidv 3259	. . 3 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
8		eqeq1 2802	. . . . . . 7 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (𝑞 = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩))
9	8	3anbi2d 1438	. . . . . 6 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
10	9	rexbidv 3256	. . . . 5 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
11	10	2rexbidv 3259	. . . 4 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
12	11	2rexbidv 3259	. . 3 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
13		br4.6	. . 3 ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}
14	1, 2, 7, 12, 13	brab 5395	. 2 ⊢ (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
15		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
16		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
17	15, 16	opth 5333	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵))
18		br4.1	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
19		br4.2	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
20	18, 19	sylan9bb 513	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒))
21	17, 20	sylbi 220	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ 𝜒))
22	21	eqcoms 2806	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))
23		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
24		vex 3444	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
25	23, 24	opth 5333	. . . . . . . . . . 11 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))
26		br4.3	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
27		br4.4	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
28	26, 27	sylan9bb 513	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏))
29	25, 28	sylbi 220	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜒 ↔ 𝜏))
30	29	eqcoms 2806	. . . . . . . . 9 ⊢ (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ → (𝜒 ↔ 𝜏))
31	22, 30	sylan9bb 513	. . . . . . . 8 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩) → (𝜑 ↔ 𝜏))
32	31	biimp3a 1466	. . . . . . 7 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏)
33	32	a1i 11	. . . . . 6 ⊢ (((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ 𝑑 ∈ 𝑃) → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
34	33	rexlimdva 3243	. . . . 5 ⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
35	34	rexlimdvva 3253	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
36	35	rexlimdvva 3253	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
37		simpl1 1188	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝑋 ∈ 𝑆)
38		simpl2l 1223	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐴 ∈ 𝑄)
39		simpl2r 1224	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐵 ∈ 𝑄)
40		simpl3l 1225	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐶 ∈ 𝑄)
41		simpl3r 1226	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐷 ∈ 𝑄)
42		eqidd 2799	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
43		eqidd 2799	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
44		simpr 488	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝜏)
45		opeq1 4763	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
46	45	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩))
47	46, 26	3anbi23d 1436	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃)))
48		opeq2 4765	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
49	48	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩))
50	49, 27	3anbi23d 1436	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)))
51	47, 50	rspc2ev 3583	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
52	40, 41, 42, 43, 44, 51	syl113anc 1379	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
53		opeq1 4763	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
54	53	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩))
55	54, 18	3anbi13d 1435	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
56	55	2rexbidv 3259	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
57		opeq2 4765	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
58	57	eqeq2d 2809	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
59	58, 19	3anbi13d 1435	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
60	59	2rexbidv 3259	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
61	56, 60	rspc2ev 3583	. . . . . 6 ⊢ ((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
62	38, 39, 52, 61	syl3anc 1368	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
63		br4.5	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
64	63	rexeqdv 3365	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
65	63, 64	rexeqbidv 3355	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
66	63, 65	rexeqbidv 3355	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
67	63, 66	rexeqbidv 3355	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
68	67	rspcev 3571	. . . . 5 ⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
69	37, 62, 68	syl2anc 587	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
70	69	ex 416	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (𝜏 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
71	36, 70	impbid 215	. 2 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ 𝜏))
72	14, 71	syl5bb 286	1 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 399 ∧ w3a 1084 = wceq 1538 ∈ wcel 2111 ∃wrex 3107 ⟨cop 4531 class class class wbr 5030 {copab 5092

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1911 ax-6 1970 ax-7 2015 ax-8 2113 ax-9 2121 ax-10 2142 ax-11 2158 ax-12 2175 ax-ext 2770 ax-sep 5167 ax-nul 5174 ax-pr 5295

This theorem depends on definitions: df-bi 210 df-an 400 df-or 845 df-3an 1086 df-tru 1541 df-ex 1782 df-nf 1786 df-sb 2070 df-mo 2598 df-eu 2629 df-clab 2777 df-cleq 2791 df-clel 2870 df-nfc 2938 df-ral 3111 df-rex 3112 df-v 3443 df-dif 3884 df-un 3886 df-in 3888 df-ss 3898 df-nul 4244 df-if 4426 df-sn 4526 df-pr 4528 df-op 4532 df-br 5031 df-opab 5093

This theorem is referenced by: (None)

W3C validator