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 34330

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 5421	. . 3 ⊢ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∈ V
2		opex 5421	. . 3 ⊢ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∈ V
3		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩))
4		eqcom 2743	. . . . . . . . 9 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
5	3, 4	bitrdi 286	. . . . . . . 8 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
6	5	3anbi1d 1440	. . . . . . 7 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → ((𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
7	6	rexbidv 3175	. . . . . 6 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
8	7	2rexbidv 3213	. . . . 5 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
9	8	2rexbidv 3213	. . . 4 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
10	9	2rexbidv 3213	. . 3 ⊢ (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
11		eqeq1 2740	. . . . . . . . 9 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩))
12		eqcom 2743	. . . . . . . . 9 ⊢ (⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
13	11, 12	bitrdi 286	. . . . . . . 8 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
14	13	3anbi2d 1441	. . . . . . 7 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
15	14	rexbidv 3175	. . . . . 6 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
16	15	2rexbidv 3213	. . . . 5 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
17	16	2rexbidv 3213	. . . 4 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
18	17	2rexbidv 3213	. . 3 ⊢ (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
19		br6.8	. . 3 ⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
20	1, 2, 10, 18, 19	brab 5500	. 2 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
21		vex 3449	. . . . . . . . . . . 12 ⊢ 𝑎 ∈ V
22		opex 5421	. . . . . . . . . . . 12 ⊢ ⟨𝑏, 𝑐⟩ ∈ V
23	21, 22	opth 5433	. . . . . . . . . . 11 ⊢ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ (𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩))
24		br6.1	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓))
25		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑏 ∈ V
26		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑐 ∈ V
27	25, 26	opth 5433	. . . . . . . . . . . . 13 ⊢ (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ ↔ (𝑏 = 𝐵 ∧ 𝑐 = 𝐶))
28		br6.2	. . . . . . . . . . . . . 14 ⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒))
29		br6.3	. . . . . . . . . . . . . 14 ⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃))
30	28, 29	sylan9bb 510	. . . . . . . . . . . . 13 ⊢ ((𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜓 ↔ 𝜃))
31	27, 30	sylbi 216	. . . . . . . . . . . 12 ⊢ (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ → (𝜓 ↔ 𝜃))
32	24, 31	sylan9bb 510	. . . . . . . . . . 11 ⊢ ((𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩) → (𝜑 ↔ 𝜃))
33	23, 32	sylbi 216	. . . . . . . . . 10 ⊢ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝜑 ↔ 𝜃))
34		vex 3449	. . . . . . . . . . . 12 ⊢ 𝑑 ∈ V
35		opex 5421	. . . . . . . . . . . 12 ⊢ ⟨𝑒, 𝑓⟩ ∈ V
36	34, 35	opth 5433	. . . . . . . . . . 11 ⊢ (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩))
37		br6.4	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏))
38		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑒 ∈ V
39		vex 3449	. . . . . . . . . . . . . 14 ⊢ 𝑓 ∈ V
40	38, 39	opth 5433	. . . . . . . . . . . . 13 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹))
41		br6.5	. . . . . . . . . . . . . 14 ⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂))
42		br6.6	. . . . . . . . . . . . . 14 ⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁))
43	41, 42	sylan9bb 510	. . . . . . . . . . . . 13 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜏 ↔ 𝜁))
44	40, 43	sylbi 216	. . . . . . . . . . . 12 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏 ↔ 𝜁))
45	37, 44	sylan9bb 510	. . . . . . . . . . 11 ⊢ ((𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩) → (𝜃 ↔ 𝜁))
46	36, 45	sylbi 216	. . . . . . . . . 10 ⊢ (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝜃 ↔ 𝜁))
47	33, 46	sylan9bb 510	. . . . . . . . 9 ⊢ ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) → (𝜑 ↔ 𝜁))
48	47	biimp3a 1469	. . . . . . . 8 ⊢ ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁)
49	48	a1i 11	. . . . . . 7 ⊢ ((((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ 𝑓 ∈ 𝑃) → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
50	49	rexlimdva 3152	. . . . . 6 ⊢ (((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
51	50	rexlimdvva 3205	. . . . 5 ⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
52	51	rexlimdvva 3205	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
53	52	rexlimdvva 3205	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
54		simpl1 1191	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → 𝑋 ∈ 𝑆)
55		simpl2 1192	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄))
56		opeq1 4830	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝑒, 𝑓⟩⟩)
57	56	eqeq1d 2738	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
58	57, 37	3anbi23d 1439	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏)))
59		opeq1 4830	. . . . . . . . . . 11 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
60	59	opeq2d 4837	. . . . . . . . . 10 ⊢ (𝑒 = 𝐸 → ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝑓⟩⟩)
61	60	eqeq1d 2738	. . . . . . . . 9 ⊢ (𝑒 = 𝐸 → (⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
62	61, 41	3anbi23d 1439	. . . . . . . 8 ⊢ (𝑒 = 𝐸 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂)))
63		opeq2 4831	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
64	63	opeq2d 4837	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
65	64	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
66	65, 42	3anbi23d 1439	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁)))
67		eqid 2736	. . . . . . . . . . 11 ⊢ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩
68		eqid 2736	. . . . . . . . . . 11 ⊢ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩
69	67, 68	pm3.2i 471	. . . . . . . . . 10 ⊢ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
70		df-3an 1089	. . . . . . . . . 10 ⊢ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) ∧ 𝜁))
71	69, 70	mpbiran 707	. . . . . . . . 9 ⊢ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ 𝜁)
72	66, 71	bitrdi 286	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ 𝜁))
73	58, 62, 72	rspc3ev 3594	. . . . . . 7 ⊢ (((𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
74	73	3ad2antl3 1187	. . . . . 6 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
75		opeq1 4830	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
76	75	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
77	76, 24	3anbi13d 1438	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
78	77	rexbidv 3175	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
79	78	2rexbidv 3213	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
80		opeq1 4830	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
81	80	opeq2d 4837	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
82	81	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
83	82, 28	3anbi13d 1438	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → ((⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
84	83	rexbidv 3175	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
85	84	2rexbidv 3213	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
86		opeq2 4831	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
87	86	opeq2d 4837	. . . . . . . . . . 11 ⊢ (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
88	87	eqeq1d 2738	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
89	88, 29	3anbi13d 1438	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → ((⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
90	89	rexbidv 3175	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
91	90	2rexbidv 3213	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
92	79, 85, 91	rspc3ev 3594	. . . . . 6 ⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
93	55, 74, 92	syl2anc 584	. . . . 5 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
94		br6.7	. . . . . . 7 ⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄)
95	94	rexeqdv 3314	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑋 → (∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
96	94, 95	rexeqbidv 3320	. . . . . . . . . 10 ⊢ (𝑥 = 𝑋 → (∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
97	94, 96	rexeqbidv 3320	. . . . . . . . 9 ⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
98	94, 97	rexeqbidv 3320	. . . . . . . 8 ⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
99	94, 98	rexeqbidv 3320	. . . . . . 7 ⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
100	94, 99	rexeqbidv 3320	. . . . . 6 ⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
101	100	rspcev 3581	. . . . 5 ⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
102	54, 93, 101	syl2anc 584	. . . 4 ⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
103	102	ex 413	. . 3 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (𝜁 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
104	53, 103	impbid 211	. 2 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ 𝜁))
105	20, 104	bitrid 282	1 ⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 205 ∧ wa 396 ∧ w3a 1087 = wceq 1541 ∈ wcel 2106 ∃wrex 3073 ⟨cop 4592 class class class wbr 5105 {copab 5167

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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384

This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-sb 2068 df-clab 2714 df-cleq 2728 df-clel 2814 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-br 5106 df-opab 5168

This theorem is referenced by: brcgr3 34631

W3C validator