br6 - Mathbox for Scott Fenton

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

Theorem br6 36522

Description: Substitution for a six-place predicate. (Contributed by Scott Fenton, 4-Oct-2013.) (Revised by Mario Carneiro, 3-May-2015.)

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

**Assertion**
Ref	Expression
br6	⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))

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

**Proof of Theorem br6**
Step	Hyp	Ref	Expression
1		opex 5432	. . 3 ⊢ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∈ V
2		opex 5432	. . 3 ⊢ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∈ V
3		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩))
4		eqcom 2768	. . . . . . . . 9 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
5	3, 4	bitrdi 290	. . . . . . . 8 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
6	5	3anbi1d 1468	. . . . . . 7 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → ((𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
7	6	rexbidv 3187	. . . . . 6 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
8	7	2rexbidv 3228	. . . . 5 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
9	8	2rexbidv 3228	. . . 4 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
10	9	2rexbidv 3228	. . 3 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
11		eqeq1 2765	. . . . . . . . 9 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩))
12		eqcom 2768	. . . . . . . . 9 ⊢ (⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
13	11, 12	bitrdi 290	. . . . . . . 8 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
14	13	3anbi2d 1469	. . . . . . 7 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
15	14	rexbidv 3187	. . . . . 6 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
16	15	2rexbidv 3228	. . . . 5 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
17	16	2rexbidv 3228	. . . 4 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
18	17	2rexbidv 3228	. . 3 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
19		br6.8	. . 3 ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
20	1, 2, 10, 18, 19	brab 5518	. 2 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
21		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
22		opex 5432	. . . . . . . . . . . 12 ⊢ ⟨𝑏, 𝑐⟩ ∈ V
23	21, 22	opth 5445	. . . . . . . . . . 11 ⊢ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ (𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩))
24		br6.1	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
25		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
26		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
27	25, 26	opth 5445	. . . . . . . . . . . . 13 ⊢ (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ ↔ (𝑏 = 𝐵 ∧ 𝑐 = 𝐶))
28		br6.2	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
29		br6.3	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
30	28, 29	sylan9bb 519	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜓 ↔ 𝜃))
31	27, 30	sylbi 220	. . . . . . . . . . . 12 ⊢ (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ → (𝜓 ↔ 𝜃))
32	24, 31	sylan9bb 519	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩) → (𝜑 ↔ 𝜃))
33	23, 32	sylbi 220	. . . . . . . . . 10 ⊢ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝜑 ↔ 𝜃))
34		vex 3455	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
35		opex 5432	. . . . . . . . . . . 12 ⊢ ⟨𝑒, 𝑓⟩ ∈ V
36	34, 35	opth 5445	. . . . . . . . . . 11 ⊢ (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩))
37		br6.4	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
38		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑒 ∈ V
39		vex 3455	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
40	38, 39	opth 5445	. . . . . . . . . . . . 13 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹))
41		br6.5	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))
42		br6.6	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))
43	41, 42	sylan9bb 519	. . . . . . . . . . . . 13 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜏 ↔ 𝜁))
44	40, 43	sylbi 220	. . . . . . . . . . . 12 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏 ↔ 𝜁))
45	37, 44	sylan9bb 519	. . . . . . . . . . 11 ⊢ ((𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩) → (𝜃 ↔ 𝜁))
46	36, 45	sylbi 220	. . . . . . . . . 10 ⊢ (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝜃 ↔ 𝜁))
47	33, 46	sylan9bb 519	. . . . . . . . 9 ⊢ ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) → (𝜑 ↔ 𝜁))
48	47	biimp3a 1498	. . . . . . . 8 ⊢ ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁)
49	48	a1i 11	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ 𝑓 ∈ 𝑃) → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
50	49	rexlimdva 3164	. . . . . 6 ⊢ (((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
51	50	rexlimdvva 3220	. . . . 5 ⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
52	51	rexlimdvva 3220	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
53	52	rexlimdvva 3220	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
54		simpl1 1210	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → 𝑋 ∈ 𝑆)
55		simpl2 1211	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄))
56		opeq1 4833	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝑒, 𝑓⟩⟩)
57	56	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
58	57, 37	3anbi23d 1467	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏)))
59		opeq1 4833	. . . . . . . . . . 11 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
60	59	opeq2d 4840	. . . . . . . . . 10 ⊢ (𝑒 = 𝐸 → ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝑓⟩⟩)
61	60	eqeq1d 2763	. . . . . . . . 9 ⊢ (𝑒 = 𝐸 → (⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
62	61, 41	3anbi23d 1467	. . . . . . . 8 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂)))
63		opeq2 4834	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
64	63	opeq2d 4840	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
65	64	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
66	65, 42	3anbi23d 1467	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁)))
67		eqid 2761	. . . . . . . . . . 11 ⊢ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩
68		eqid 2761	. . . . . . . . . . 11 ⊢ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩
69	67, 68	pm3.2i 476	. . . . . . . . . 10 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
70		df-3an 1105	. . . . . . . . . 10 ⊢ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) ∧ 𝜁))
71	69, 70	mpbiran 722	. . . . . . . . 9 ⊢ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ 𝜁)
72	66, 71	bitrdi 290	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ 𝜁))
73	58, 62, 72	rspc3ev 3593	. . . . . . 7 ⊢ (((𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
74	73	3ad2antl3 1206	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
75		opeq1 4833	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
76	75	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
77	76, 24	3anbi13d 1466	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
78	77	rexbidv 3187	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
79	78	2rexbidv 3228	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
80		opeq1 4833	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
81	80	opeq2d 4840	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
82	81	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
83	82, 28	3anbi13d 1466	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
84	83	rexbidv 3187	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
85	84	2rexbidv 3228	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
86		opeq2 4834	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
87	86	opeq2d 4840	. . . . . . . . . . 11 ⊢ (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
88	87	eqeq1d 2763	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
89	88, 29	3anbi13d 1466	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
90	89	rexbidv 3187	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
91	90	2rexbidv 3228	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
92	79, 85, 91	rspc3ev 3593	. . . . . 6 ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
93	55, 74, 92	syl2anc 596	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
94		br6.7	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
95	94	rexeqdv 3321	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
96	94, 95	rexeqbidv 3336	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
97	94, 96	rexeqbidv 3336	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
98	94, 97	rexeqbidv 3336	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
99	94, 98	rexeqbidv 3336	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
100	94, 99	rexeqbidv 3336	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
101	100	rspcev 3577	. . . . 5 ⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
102	54, 93, 101	syl2anc 596	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
103	102	ex 418	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (𝜁 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
104	53, 103	impbid 215	. 2 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ 𝜁))
105	20, 104	bitrid 286	1 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ∈ wcel 2145 ∃wrex 3087 ⟨cop 4590 class class class wbr 5103 {copab 5167

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-ext 2733 ax-sep 5249 ax-pr 5391

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-sb 2100 df-clab 2740 df-cleq 2753 df-clel 2836 df-ral 3078 df-rex 3088 df-rab 3414 df-v 3453 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-nul 4280 df-if 4483 df-sn 4585 df-pr 4587 df-op 4591 df-br 5104 df-opab 5168

This theorem is used by: brcgr3 36811

W3C validator