br8d - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > br8d		Structured version Visualization version GIF version

Theorem br8d 28802

Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.) (Revised by Thierry Arnoux, 21-Mar-2019.)

**Hypotheses**
Ref	Expression
br8d.1	⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒))
br8d.2	⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃))
br8d.3	⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏))
br8d.4	⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂))
br8d.5	⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁))
br8d.6	⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎))
br8d.7	⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌))
br8d.8	⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇))
br8d.10	⊢ (𝜑 → 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)})
br8d.11	⊢ (𝜑 → 𝐴 ∈ 𝑃)
br8d.12	⊢ (𝜑 → 𝐵 ∈ 𝑃)
br8d.13	⊢ (𝜑 → 𝐶 ∈ 𝑃)
br8d.14	⊢ (𝜑 → 𝐷 ∈ 𝑃)
br8d.15	⊢ (𝜑 → 𝐸 ∈ 𝑃)
br8d.16	⊢ (𝜑 → 𝐹 ∈ 𝑃)
br8d.17	⊢ (𝜑 → 𝐺 ∈ 𝑃)
br8d.18	⊢ (𝜑 → 𝐻 ∈ 𝑃)

**Assertion**
Ref	Expression
br8d	⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇))

Distinct variable groups: 𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞,𝐴 𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐺,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝐻,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝑃,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ,𝑝,𝑞 𝜒,𝑎 𝜃,𝑏 𝜏,𝑐 𝜂,𝑑 𝜁,𝑒 𝜎,𝑓 𝜌,𝑔 𝜓,𝑝,𝑞 𝜇,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,ℎ Allowed substitution hints: 𝜑(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜓(𝑒,𝑓,𝑔,ℎ,𝑎,𝑏,𝑐,𝑑) 𝜒(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑏,𝑐,𝑑) 𝜃(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑐,𝑑) 𝜏(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑑) 𝜂(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐) 𝜁(𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜎(𝑒,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜌(𝑒,𝑓,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑) 𝜇(𝑞,𝑝) 𝑅(𝑒,𝑓,𝑔,ℎ,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)

**Proof of Theorem br8d**
Step	Hyp	Ref	Expression
1		br8d.10	. . . 4 ⊢ (𝜑 → 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)})
2	1	breqd 4594	. . 3 ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
3		opex 4859	. . . 4 ⊢ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∈ V
4		opex 4859	. . . 4 ⊢ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∈ V
5		eqeq1 2614	. . . . . . . . . 10 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
6	5	3anbi1d 1395	. . . . . . . . 9 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → ((𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
7	6	rexbidv 3034	. . . . . . . 8 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
8	7	2rexbidv 3039	. . . . . . 7 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
9	8	2rexbidv 3039	. . . . . 6 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
10	9	2rexbidv 3039	. . . . 5 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
11	10	rexbidv 3034	. . . 4 ⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
12		eqeq1 2614	. . . . . . . . . 10 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩))
13	12	3anbi2d 1396	. . . . . . . . 9 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
14	13	rexbidv 3034	. . . . . . . 8 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
15	14	2rexbidv 3039	. . . . . . 7 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
16	15	2rexbidv 3039	. . . . . 6 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
17	16	2rexbidv 3039	. . . . 5 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
18	17	rexbidv 3034	. . . 4 ⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
19		eqid 2610	. . . 4 ⊢ {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)} = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)}
20	3, 4, 11, 18, 19	brab 4923	. . 3 ⊢ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))
21	2, 20	syl6bb 275	. 2 ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
22		br8d.11	. . 3 ⊢ (𝜑 → 𝐴 ∈ 𝑃)
23		br8d.12	. . 3 ⊢ (𝜑 → 𝐵 ∈ 𝑃)
24		br8d.13	. . 3 ⊢ (𝜑 → 𝐶 ∈ 𝑃)
25		br8d.14	. . 3 ⊢ (𝜑 → 𝐷 ∈ 𝑃)
26		br8d.15	. . 3 ⊢ (𝜑 → 𝐸 ∈ 𝑃)
27		br8d.16	. . 3 ⊢ (𝜑 → 𝐹 ∈ 𝑃)
28		br8d.17	. . 3 ⊢ (𝜑 → 𝐺 ∈ 𝑃)
29		br8d.18	. . 3 ⊢ (𝜑 → 𝐻 ∈ 𝑃)
30		opex 4859	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑎, 𝑏⟩ ∈ V
31		opex 4859	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑐, 𝑑⟩ ∈ V
32	30, 31	opth 4871	. . . . . . . . . . . . . 14 ⊢ (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ↔ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩))
33		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑎 ∈ V
34		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑏 ∈ V
35	33, 34	opth 4871	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵))
36		br8d.1	. . . . . . . . . . . . . . . . 17 ⊢ (𝑎 = 𝐴 → (𝜓 ↔ 𝜒))
37		br8d.2	. . . . . . . . . . . . . . . . 17 ⊢ (𝑏 = 𝐵 → (𝜒 ↔ 𝜃))
38	36, 37	sylan9bb 732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜓 ↔ 𝜃))
39	35, 38	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜓 ↔ 𝜃))
40		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑐 ∈ V
41		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑑 ∈ V
42	40, 41	opth 4871	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷))
43		br8d.3	. . . . . . . . . . . . . . . . 17 ⊢ (𝑐 = 𝐶 → (𝜃 ↔ 𝜏))
44		br8d.4	. . . . . . . . . . . . . . . . 17 ⊢ (𝑑 = 𝐷 → (𝜏 ↔ 𝜂))
45	43, 44	sylan9bb 732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜃 ↔ 𝜂))
46	42, 45	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜃 ↔ 𝜂))
47	39, 46	sylan9bb 732	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩) → (𝜓 ↔ 𝜂))
48	32, 47	sylbi 206	. . . . . . . . . . . . 13 ⊢ (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝜓 ↔ 𝜂))
49	48	eqcoms 2618	. . . . . . . . . . . 12 ⊢ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ → (𝜓 ↔ 𝜂))
50		opex 4859	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑒, 𝑓⟩ ∈ V
51		opex 4859	. . . . . . . . . . . . . . 15 ⊢ ⟨𝑔, ℎ⟩ ∈ V
52	50, 51	opth 4871	. . . . . . . . . . . . . 14 ⊢ (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩))
53		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑒 ∈ V
54		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑓 ∈ V
55	53, 54	opth 4871	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹))
56		br8d.5	. . . . . . . . . . . . . . . . 17 ⊢ (𝑒 = 𝐸 → (𝜂 ↔ 𝜁))
57		br8d.6	. . . . . . . . . . . . . . . . 17 ⊢ (𝑓 = 𝐹 → (𝜁 ↔ 𝜎))
58	56, 57	sylan9bb 732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜂 ↔ 𝜎))
59	55, 58	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜂 ↔ 𝜎))
60		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ 𝑔 ∈ V
61		vex 3176	. . . . . . . . . . . . . . . . 17 ⊢ ℎ ∈ V
62	60, 61	opth 4871	. . . . . . . . . . . . . . . 16 ⊢ (⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩ ↔ (𝑔 = 𝐺 ∧ ℎ = 𝐻))
63		br8d.7	. . . . . . . . . . . . . . . . 17 ⊢ (𝑔 = 𝐺 → (𝜎 ↔ 𝜌))
64		br8d.8	. . . . . . . . . . . . . . . . 17 ⊢ (ℎ = 𝐻 → (𝜌 ↔ 𝜇))
65	63, 64	sylan9bb 732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (𝜎 ↔ 𝜇))
66	62, 65	sylbi 206	. . . . . . . . . . . . . . 15 ⊢ (⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩ → (𝜎 ↔ 𝜇))
67	59, 66	sylan9bb 732	. . . . . . . . . . . . . 14 ⊢ ((⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩) → (𝜂 ↔ 𝜇))
68	52, 67	sylbi 206	. . . . . . . . . . . . 13 ⊢ (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝜂 ↔ 𝜇))
69	68	eqcoms 2618	. . . . . . . . . . . 12 ⊢ (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ → (𝜂 ↔ 𝜇))
70	49, 69	sylan9bb 732	. . . . . . . . . . 11 ⊢ ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩) → (𝜓 ↔ 𝜇))
71	70	biimp3a 1424	. . . . . . . . . 10 ⊢ ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇)
72	71	a1i 11	. . . . . . . . 9 ⊢ ((((((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝑎 ∈ 𝑃) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) ∧ ℎ ∈ 𝑃) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
73	72	rexlimdva 3013	. . . . . . . 8 ⊢ (((((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝑎 ∈ 𝑃) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
74	73	rexlimdvva 3020	. . . . . . 7 ⊢ ((((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝑎 ∈ 𝑃) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
75	74	rexlimdvva 3020	. . . . . 6 ⊢ (((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝑎 ∈ 𝑃) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
76	75	rexlimdvva 3020	. . . . 5 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝑎 ∈ 𝑃) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
77	76	rexlimdva 3013	. . . 4 ⊢ (((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) → 𝜇))
78		simpl1l 1105	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐴 ∈ 𝑃)
79		simpl1r 1106	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐵 ∈ 𝑃)
80		simpl21 1132	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐶 ∈ 𝑃)
81		simpl22 1133	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐷 ∈ 𝑃)
82		simpl23 1134	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐸 ∈ 𝑃)
83		simpl31 1135	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐹 ∈ 𝑃)
84		simpl32 1136	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐺 ∈ 𝑃)
85		simpl33 1137	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝐻 ∈ 𝑃)
86		eqidd 2611	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
87		eqidd 2611	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
88		simpr 476	. . . . . . . 8 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → 𝜇)
89		opeq1 4340	. . . . . . . . . . . 12 ⊢ (𝑔 = 𝐺 → ⟨𝑔, ℎ⟩ = ⟨𝐺, ℎ⟩)
90	89	opeq2d 4347	. . . . . . . . . . 11 ⊢ (𝑔 = 𝐺 → ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩)
91	90	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑔 = 𝐺 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩))
92	91, 63	3anbi23d 1394	. . . . . . . . 9 ⊢ (𝑔 = 𝐺 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ∧ 𝜌)))
93		opeq2 4341	. . . . . . . . . . . 12 ⊢ (ℎ = 𝐻 → ⟨𝐺, ℎ⟩ = ⟨𝐺, 𝐻⟩)
94	93	opeq2d 4347	. . . . . . . . . . 11 ⊢ (ℎ = 𝐻 → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
95	94	eqeq2d 2620	. . . . . . . . . 10 ⊢ (ℎ = 𝐻 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
96	95, 64	3anbi23d 1394	. . . . . . . . 9 ⊢ (ℎ = 𝐻 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ∧ 𝜌) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)))
97	92, 96	rspc2ev 3295	. . . . . . . 8 ⊢ ((𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃 ∧ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)) → ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎))
98	84, 85, 86, 87, 88, 97	syl113anc 1330	. . . . . . 7 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎))
99		opeq2 4341	. . . . . . . . . . . 12 ⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
100	99	opeq2d 4347	. . . . . . . . . . 11 ⊢ (𝑑 = 𝐷 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
101	100	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑑 = 𝐷 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
102	101, 44	3anbi13d 1393	. . . . . . . . 9 ⊢ (𝑑 = 𝐷 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂)))
103	102	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑑 = 𝐷 → (∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏) ↔ ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂)))
104		opeq1 4340	. . . . . . . . . . . 12 ⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
105	104	opeq1d 4346	. . . . . . . . . . 11 ⊢ (𝑒 = 𝐸 → ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩)
106	105	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑒 = 𝐸 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩))
107	106, 56	3anbi23d 1394	. . . . . . . . 9 ⊢ (𝑒 = 𝐸 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁)))
108	107	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑒 = 𝐸 → (∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂) ↔ ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁)))
109		opeq2 4341	. . . . . . . . . . . 12 ⊢ (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
110	109	opeq1d 4346	. . . . . . . . . . 11 ⊢ (𝑓 = 𝐹 → ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩)
111	110	eqeq2d 2620	. . . . . . . . . 10 ⊢ (𝑓 = 𝐹 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩))
112	111, 57	3anbi23d 1394	. . . . . . . . 9 ⊢ (𝑓 = 𝐹 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎)))
113	112	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑓 = 𝐹 → (∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁) ↔ ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎)))
114	103, 108, 113	rspc3ev 3297	. . . . . . 7 ⊢ (((𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃 ∧ 𝐹 ∈ 𝑃) ∧ ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜎)) → ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏))
115	81, 82, 83, 98, 114	syl31anc 1321	. . . . . 6 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏))
116		opeq1 4340	. . . . . . . . . . . . 13 ⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
117	116	opeq1d 4346	. . . . . . . . . . . 12 ⊢ (𝑎 = 𝐴 → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
118	117	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑎 = 𝐴 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
119	118, 36	3anbi13d 1393	. . . . . . . . . 10 ⊢ (𝑎 = 𝐴 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒)))
120	119	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑎 = 𝐴 → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒)))
121	120	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒)))
122	121	2rexbidv 3039	. . . . . . 7 ⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒)))
123		opeq2 4341	. . . . . . . . . . . . 13 ⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
124	123	opeq1d 4346	. . . . . . . . . . . 12 ⊢ (𝑏 = 𝐵 → ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩)
125	124	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑏 = 𝐵 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩))
126	125, 37	3anbi13d 1393	. . . . . . . . . 10 ⊢ (𝑏 = 𝐵 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)))
127	126	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑏 = 𝐵 → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)))
128	127	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)))
129	128	2rexbidv 3039	. . . . . . 7 ⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)))
130		opeq1 4340	. . . . . . . . . . . . 13 ⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
131	130	opeq2d 4347	. . . . . . . . . . . 12 ⊢ (𝑐 = 𝐶 → ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩)
132	131	eqeq2d 2620	. . . . . . . . . . 11 ⊢ (𝑐 = 𝐶 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩))
133	132, 43	3anbi13d 1393	. . . . . . . . . 10 ⊢ (𝑐 = 𝐶 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏)))
134	133	rexbidv 3034	. . . . . . . . 9 ⊢ (𝑐 = 𝐶 → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏)))
135	134	2rexbidv 3039	. . . . . . . 8 ⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏)))
136	135	2rexbidv 3039	. . . . . . 7 ⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏)))
137	122, 129, 136	rspc3ev 3297	. . . . . 6 ⊢ (((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃 ∧ 𝐶 ∈ 𝑃) ∧ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏)) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))
138	78, 79, 80, 115, 137	syl31anc 1321	. . . . 5 ⊢ ((((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) ∧ 𝜇) → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))
139	138	ex 449	. . . 4 ⊢ (((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) → (𝜇 → ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓)))
140	77, 139	impbid 201	. . 3 ⊢ (((𝐴 ∈ 𝑃 ∧ 𝐵 ∈ 𝑃) ∧ (𝐶 ∈ 𝑃 ∧ 𝐷 ∈ 𝑃 ∧ 𝐸 ∈ 𝑃) ∧ (𝐹 ∈ 𝑃 ∧ 𝐺 ∈ 𝑃 ∧ 𝐻 ∈ 𝑃)) → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ 𝜇))
141	22, 23, 24, 25, 26, 27, 28, 29, 140	syl233anc 1347	. 2 ⊢ (𝜑 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ 𝜇))
142	21, 141	bitrd 267	1 ⊢ (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 195 ∧ wa 383 ∧ w3a 1031 = wceq 1475 ∈ wcel 1977 ∃wrex 2897 ⟨cop 4131 class class class wbr 4583 {copab 4642

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1713 ax-4 1728 ax-5 1827 ax-6 1875 ax-7 1922 ax-9 1986 ax-10 2006 ax-11 2021 ax-12 2034 ax-13 2234 ax-ext 2590 ax-sep 4709 ax-nul 4717 ax-pr 4833

This theorem depends on definitions: df-bi 196 df-or 384 df-an 385 df-3an 1033 df-tru 1478 df-ex 1696 df-nf 1701 df-sb 1868 df-eu 2462 df-mo 2463 df-clab 2597 df-cleq 2603 df-clel 2606 df-nfc 2740 df-ral 2901 df-rex 2902 df-rab 2905 df-v 3175 df-dif 3543 df-un 3545 df-in 3547 df-ss 3554 df-nul 3875 df-if 4037 df-sn 4126 df-pr 4128 df-op 4132 df-br 4584 df-opab 4644

This theorem is referenced by: brafs 30003

W3C validator