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 36105

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 5431	. . 3 ⊢ ⟨𝐴, 𝐵⟩ ∈ V
2		opex 5431	. . 3 ⊢ ⟨𝐶, 𝐷⟩ ∈ V
3		eqeq1 2766	. . . . . . 7 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (𝑝 = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩))
4	3	3anbi1d 1461	. . . . . 6 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → ((𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
5	4	rexbidv 3186	. . . . 5 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
6	5	2rexbidv 3227	. . . 4 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
7	6	2rexbidv 3227	. . 3 ⊢ (𝑝 = ⟨𝐴, 𝐵⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
8		eqeq1 2766	. . . . . . 7 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (𝑞 = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩))
9	8	3anbi2d 1462	. . . . . 6 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
10	9	rexbidv 3186	. . . . 5 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
11	10	2rexbidv 3227	. . . 4 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
12	11	2rexbidv 3227	. . 3 ⊢ (𝑞 = ⟨𝐶, 𝐷⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
13		br4.6	. . 3 ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (𝑝 = ⟨𝑎, 𝑏⟩ ∧ 𝑞 = ⟨𝑐, 𝑑⟩ ∧ 𝜑)}
14	1, 2, 7, 12, 13	brab 5514	. 2 ⊢ (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
15		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
16		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑏 ∈ V
17	15, 16	opth 5444	. . . . . . . . . . 11 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵))
18		br4.1	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
19		br4.2	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
20	18, 19	sylan9bb 517	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒))
21	17, 20	sylbi 219	. . . . . . . . . 10 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ 𝜒))
22	21	eqcoms 2770	. . . . . . . . 9 ⊢ (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ → (𝜑 ↔ 𝜒))
23		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑐 ∈ V
24		vex 3458	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
25	23, 24	opth 5444	. . . . . . . . . . 11 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))
26		br4.3	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
27		br4.4	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
28	26, 27	sylan9bb 517	. . . . . . . . . . 11 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏))
29	25, 28	sylbi 219	. . . . . . . . . 10 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜒 ↔ 𝜏))
30	29	eqcoms 2770	. . . . . . . . 9 ⊢ (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ → (𝜒 ↔ 𝜏))
31	22, 30	sylan9bb 517	. . . . . . . 8 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩) → (𝜑 ↔ 𝜏))
32	31	biimp3a 1490	. . . . . . 7 ⊢ ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏)
33	32	a1i 11	. . . . . 6 ⊢ (((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ 𝑑 ∈ 𝑃) → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
34	33	rexlimdva 3163	. . . . 5 ⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
35	34	rexlimdvva 3219	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
36	35	rexlimdvva 3219	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) → 𝜏))
37		simpl1 1205	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝑋 ∈ 𝑆)
38		simpl2l 1240	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐴 ∈ 𝑄)
39		simpl2r 1241	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐵 ∈ 𝑄)
40		simpl3l 1242	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐶 ∈ 𝑄)
41		simpl3r 1243	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝐷 ∈ 𝑄)
42		eqidd 2763	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩)
43		eqidd 2763	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩)
44		simpr 488	. . . . . . 7 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → 𝜏)
45		opeq1 4831	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
46	45	eqeq2d 2773	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩))
47	46, 26	3anbi23d 1460	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃)))
48		opeq2 4832	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
49	48	eqeq2d 2773	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ↔ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩))
50	49, 27	3anbi23d 1460	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝑑⟩ ∧ 𝜃) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)))
51	47, 50	rspc2ev 3594	. . . . . . 7 ⊢ ((𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝐶, 𝐷⟩ ∧ 𝜏)) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
52	40, 41, 42, 43, 44, 51	syl113anc 1401	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒))
53		opeq1 4831	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
54	53	eqeq2d 2773	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩))
55	54, 18	3anbi13d 1459	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → ((⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
56	55	2rexbidv 3227	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓)))
57		opeq2 4832	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
58	57	eqeq2d 2773	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ↔ ⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩))
59	58, 19	3anbi13d 1459	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
60	59	2rexbidv 3227	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜓) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)))
61	56, 60	rspc2ev 3594	. . . . . 6 ⊢ ((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜒)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
62	38, 39, 52, 61	syl3anc 1390	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
63		br4.5	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
64	63	rexeqdv 3321	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
65	63, 64	rexeqbidv 3337	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
66	63, 65	rexeqbidv 3337	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
67	63, 66	rexeqbidv 3337	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
68	67	rspcev 3581	. . . . 5 ⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
69	37, 62, 68	syl2anc 593	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) ∧ 𝜏) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑))
70	69	ex 416	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (𝜏 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑)))
71	36, 70	impbid 214	. 2 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 (⟨𝐴, 𝐵⟩ = ⟨𝑎, 𝑏⟩ ∧ ⟨𝐶, 𝐷⟩ = ⟨𝑐, 𝑑⟩ ∧ 𝜑) ↔ 𝜏))
72	14, 71	bitrid 285	1 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄)) → (⟨𝐴, 𝐵⟩𝑅⟨𝐶, 𝐷⟩ ↔ 𝜏))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 208 ∧ wa 399 ∧ w3a 1098 = wceq 1560 ∈ wcel 2142 ∃wrex 3086 ⟨cop 4588 class class class wbr 5100 {copab 5162

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1815 ax-4 1829 ax-5 1930 ax-6 1987 ax-7 2028 ax-8 2144 ax-9 2152 ax-ext 2734 ax-sep 5246 ax-pr 5390

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3an 1100 df-tru 1563 df-fal 1573 df-ex 1800 df-sb 2091 df-clab 2741 df-cleq 2754 df-clel 2837 df-ral 3077 df-rex 3087 df-rab 3415 df-v 3456 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-nul 4286 df-if 4481 df-sn 4583 df-pr 4585 df-op 4589 df-br 5101 df-opab 5163

This theorem is referenced by: (None)

W3C validator