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

Theorem br8 30733
Description: Substitution for an eight-place predicate. (Contributed by Scott Fenton, 26-Sep-2013.) (Revised by Mario Carneiro, 3-May-2015.)
Hypotheses
Ref Expression
br8.1 (𝑎 = 𝐴 → (𝜑𝜓))
br8.2 (𝑏 = 𝐵 → (𝜓𝜒))
br8.3 (𝑐 = 𝐶 → (𝜒𝜃))
br8.4 (𝑑 = 𝐷 → (𝜃𝜏))
br8.5 (𝑒 = 𝐸 → (𝜏𝜂))
br8.6 (𝑓 = 𝐹 → (𝜂𝜁))
br8.7 (𝑔 = 𝐺 → (𝜁𝜎))
br8.8 ( = 𝐻 → (𝜎𝜌))
br8.9 (𝑥 = 𝑋𝑃 = 𝑄)
br8.10 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)}
Assertion
Ref Expression
br8 (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Distinct variable groups:   𝜒,𝑏   𝜂,𝑒   𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑃   𝜓,𝑎   𝜎,𝑔   𝑥,𝑎,𝐴,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞   𝜑,𝑝,𝑞,𝑥   𝜌,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑥   𝐵,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝐶,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝜏,𝑑   𝐷,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝐸,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝜃,𝑐   𝐹,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝐺,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝜁,𝑓   𝐻,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝑆,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑝,𝑞,𝑥   𝑄,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑥   𝑋,𝑎,𝑏,𝑐,𝑑,𝑒,𝑓,𝑔,,𝑥
Allowed substitution hints:   𝜑(𝑒,𝑓,𝑔,,𝑎,𝑏,𝑐,𝑑)   𝜓(𝑥,𝑒,𝑓,𝑔,,𝑞,𝑝,𝑏,𝑐,𝑑)   𝜒(𝑥,𝑒,𝑓,𝑔,,𝑞,𝑝,𝑎,𝑐,𝑑)   𝜃(𝑥,𝑒,𝑓,𝑔,,𝑞,𝑝,𝑎,𝑏,𝑑)   𝜏(𝑥,𝑒,𝑓,𝑔,,𝑞,𝑝,𝑎,𝑏,𝑐)   𝜂(𝑥,𝑓,𝑔,,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝜁(𝑥,𝑒,𝑔,,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝜎(𝑥,𝑒,𝑓,,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝜌(𝑞,𝑝)   𝑃(𝑥)   𝑄(𝑞,𝑝)   𝑅(𝑥,𝑒,𝑓,𝑔,,𝑞,𝑝,𝑎,𝑏,𝑐,𝑑)   𝑋(𝑞,𝑝)

Proof of Theorem br8
StepHypRef Expression
1 opex 4853 . . 3 ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∈ V
2 opex 4853 . . 3 ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∈ V
3 eqeq1 2613 . . . . . . . . 9 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
433anbi1d 1394 . . . . . . . 8 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → ((𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
54rexbidv 3033 . . . . . . 7 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
652rexbidv 3038 . . . . . 6 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
762rexbidv 3038 . . . . 5 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
872rexbidv 3038 . . . 4 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
982rexbidv 3038 . . 3 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
10 eqeq1 2613 . . . . . . . . 9 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩))
11103anbi2d 1395 . . . . . . . 8 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
1211rexbidv 3033 . . . . . . 7 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
13122rexbidv 3038 . . . . . 6 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
14132rexbidv 3038 . . . . 5 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
15142rexbidv 3038 . . . 4 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
16152rexbidv 3038 . . 3 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
17 br8.10 . . 3 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)}
181, 2, 9, 16, 17brab 4913 . 2 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑))
19 opex 4853 . . . . . . . . . . . . . 14 𝑎, 𝑏⟩ ∈ V
20 opex 4853 . . . . . . . . . . . . . 14 𝑐, 𝑑⟩ ∈ V
2119, 20opth 4865 . . . . . . . . . . . . 13 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ↔ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩))
22 vex 3175 . . . . . . . . . . . . . . . 16 𝑎 ∈ V
23 vex 3175 . . . . . . . . . . . . . . . 16 𝑏 ∈ V
2422, 23opth 4865 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐵))
25 br8.1 . . . . . . . . . . . . . . . 16 (𝑎 = 𝐴 → (𝜑𝜓))
26 br8.2 . . . . . . . . . . . . . . . 16 (𝑏 = 𝐵 → (𝜓𝜒))
2725, 26sylan9bb 731 . . . . . . . . . . . . . . 15 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝜑𝜒))
2824, 27sylbi 205 . . . . . . . . . . . . . 14 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜑𝜒))
29 vex 3175 . . . . . . . . . . . . . . . 16 𝑐 ∈ V
30 vex 3175 . . . . . . . . . . . . . . . 16 𝑑 ∈ V
3129, 30opth 4865 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶𝑑 = 𝐷))
32 br8.3 . . . . . . . . . . . . . . . 16 (𝑐 = 𝐶 → (𝜒𝜃))
33 br8.4 . . . . . . . . . . . . . . . 16 (𝑑 = 𝐷 → (𝜃𝜏))
3432, 33sylan9bb 731 . . . . . . . . . . . . . . 15 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝜒𝜏))
3531, 34sylbi 205 . . . . . . . . . . . . . 14 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜒𝜏))
3628, 35sylan9bb 731 . . . . . . . . . . . . 13 ((⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩) → (𝜑𝜏))
3721, 36sylbi 205 . . . . . . . . . . . 12 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝜑𝜏))
3837eqcoms 2617 . . . . . . . . . . 11 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ → (𝜑𝜏))
39 opex 4853 . . . . . . . . . . . . . 14 𝑒, 𝑓⟩ ∈ V
40 opex 4853 . . . . . . . . . . . . . 14 𝑔, ⟩ ∈ V
4139, 40opth 4865 . . . . . . . . . . . . 13 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩))
42 vex 3175 . . . . . . . . . . . . . . . 16 𝑒 ∈ V
43 vex 3175 . . . . . . . . . . . . . . . 16 𝑓 ∈ V
4442, 43opth 4865 . . . . . . . . . . . . . . 15 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
45 br8.5 . . . . . . . . . . . . . . . 16 (𝑒 = 𝐸 → (𝜏𝜂))
46 br8.6 . . . . . . . . . . . . . . . 16 (𝑓 = 𝐹 → (𝜂𝜁))
4745, 46sylan9bb 731 . . . . . . . . . . . . . . 15 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜏𝜁))
4844, 47sylbi 205 . . . . . . . . . . . . . 14 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏𝜁))
49 vex 3175 . . . . . . . . . . . . . . . 16 𝑔 ∈ V
50 vex 3175 . . . . . . . . . . . . . . . 16 ∈ V
5149, 50opth 4865 . . . . . . . . . . . . . . 15 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ ↔ (𝑔 = 𝐺 = 𝐻))
52 br8.7 . . . . . . . . . . . . . . . 16 (𝑔 = 𝐺 → (𝜁𝜎))
53 br8.8 . . . . . . . . . . . . . . . 16 ( = 𝐻 → (𝜎𝜌))
5452, 53sylan9bb 731 . . . . . . . . . . . . . . 15 ((𝑔 = 𝐺 = 𝐻) → (𝜁𝜌))
5551, 54sylbi 205 . . . . . . . . . . . . . 14 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ → (𝜁𝜌))
5648, 55sylan9bb 731 . . . . . . . . . . . . 13 ((⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩) → (𝜏𝜌))
5741, 56sylbi 205 . . . . . . . . . . . 12 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝜏𝜌))
5857eqcoms 2617 . . . . . . . . . . 11 (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ → (𝜏𝜌))
5938, 58sylan9bb 731 . . . . . . . . . 10 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩) → (𝜑𝜌))
6059biimp3a 1423 . . . . . . . . 9 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌)
6160a1i 11 . . . . . . . 8 ((((((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) ∧ 𝑃) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
6261rexlimdva 3012 . . . . . . 7 (((((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
6362rexlimdvva 3019 . . . . . 6 ((((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
6463rexlimdvva 3019 . . . . 5 (((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
6564rexlimdvva 3019 . . . 4 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ (𝑥𝑆𝑎𝑃)) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
6665rexlimdvva 3019 . . 3 (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) → 𝜌))
67 simpl11 1128 . . . . 5 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝑋𝑆)
68 simpl12 1129 . . . . . 6 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐴𝑄)
69 simpl13 1130 . . . . . 6 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐵𝑄)
70 simpl21 1131 . . . . . 6 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐶𝑄)
71 simpl22 1132 . . . . . . 7 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐷𝑄)
72 simpl23 1133 . . . . . . 7 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐸𝑄)
73 simpl31 1134 . . . . . . 7 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐹𝑄)
74 simpl32 1135 . . . . . . . 8 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐺𝑄)
75 simpl33 1136 . . . . . . . 8 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝐻𝑄)
76 eqidd 2610 . . . . . . . 8 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
77 eqidd 2610 . . . . . . . 8 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
78 simpr 475 . . . . . . . 8 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → 𝜌)
79 opeq1 4334 . . . . . . . . . . . 12 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
8079opeq2d 4341 . . . . . . . . . . 11 (𝑔 = 𝐺 → ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩)
8180eqeq2d 2619 . . . . . . . . . 10 (𝑔 = 𝐺 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩))
8281, 523anbi23d 1393 . . . . . . . . 9 (𝑔 = 𝐺 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜎)))
83 opeq2 4335 . . . . . . . . . . . 12 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
8483opeq2d 4341 . . . . . . . . . . 11 ( = 𝐻 → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
8584eqeq2d 2619 . . . . . . . . . 10 ( = 𝐻 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
8685, 533anbi23d 1393 . . . . . . . . 9 ( = 𝐻 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜎) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜌)))
8782, 86rspc2ev 3294 . . . . . . . 8 ((𝐺𝑄𝐻𝑄 ∧ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜌)) → ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁))
8874, 75, 76, 77, 78, 87syl113anc 1329 . . . . . . 7 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁))
89 opeq2 4335 . . . . . . . . . . . 12 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
9089opeq2d 4341 . . . . . . . . . . 11 (𝑑 = 𝐷 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
9190eqeq2d 2619 . . . . . . . . . 10 (𝑑 = 𝐷 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
9291, 333anbi13d 1392 . . . . . . . . 9 (𝑑 = 𝐷 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
93922rexbidv 3038 . . . . . . . 8 (𝑑 = 𝐷 → (∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
94 opeq1 4334 . . . . . . . . . . . 12 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
9594opeq1d 4340 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩)
9695eqeq2d 2619 . . . . . . . . . 10 (𝑒 = 𝐸 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩))
9796, 453anbi23d 1393 . . . . . . . . 9 (𝑒 = 𝐸 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
98972rexbidv 3038 . . . . . . . 8 (𝑒 = 𝐸 → (∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
99 opeq2 4335 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
10099opeq1d 4340 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩)
101100eqeq2d 2619 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩))
102101, 463anbi23d 1393 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
1031022rexbidv 3038 . . . . . . . 8 (𝑓 = 𝐹 → (∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
10493, 98, 103rspc3ev 3296 . . . . . . 7 (((𝐷𝑄𝐸𝑄𝐹𝑄) ∧ ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)) → ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃))
10571, 72, 73, 88, 104syl31anc 1320 . . . . . 6 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃))
106 opeq1 4334 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
107106opeq1d 4340 . . . . . . . . . . . 12 (𝑎 = 𝐴 → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
108107eqeq2d 2619 . . . . . . . . . . 11 (𝑎 = 𝐴 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
109108, 253anbi13d 1392 . . . . . . . . . 10 (𝑎 = 𝐴 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
110109rexbidv 3033 . . . . . . . . 9 (𝑎 = 𝐴 → (∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1111102rexbidv 3038 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1121112rexbidv 3038 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
113 opeq2 4335 . . . . . . . . . . . . 13 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
114113opeq1d 4340 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩)
115114eqeq2d 2619 . . . . . . . . . . 11 (𝑏 = 𝐵 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩))
116115, 263anbi13d 1392 . . . . . . . . . 10 (𝑏 = 𝐵 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
117116rexbidv 3033 . . . . . . . . 9 (𝑏 = 𝐵 → (∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1181172rexbidv 3038 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1191182rexbidv 3038 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
120 opeq1 4334 . . . . . . . . . . . . 13 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
121120opeq2d 4341 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩)
122121eqeq2d 2619 . . . . . . . . . . 11 (𝑐 = 𝐶 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩))
123122, 323anbi13d 1392 . . . . . . . . . 10 (𝑐 = 𝐶 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
124123rexbidv 3033 . . . . . . . . 9 (𝑐 = 𝐶 → (∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1251242rexbidv 3038 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1261252rexbidv 3038 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
127112, 119, 126rspc3ev 3296 . . . . . 6 (((𝐴𝑄𝐵𝑄𝐶𝑄) ∧ ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑))
12868, 69, 70, 105, 127syl31anc 1320 . . . . 5 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑))
129 br8.9 . . . . . . 7 (𝑥 = 𝑋𝑃 = 𝑄)
130129rexeqdv 3121 . . . . . . . . . . . . 13 (𝑥 = 𝑋 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
131129, 130rexeqbidv 3129 . . . . . . . . . . . 12 (𝑥 = 𝑋 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
132129, 131rexeqbidv 3129 . . . . . . . . . . 11 (𝑥 = 𝑋 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
133129, 132rexeqbidv 3129 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
134129, 133rexeqbidv 3129 . . . . . . . . 9 (𝑥 = 𝑋 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
135129, 134rexeqbidv 3129 . . . . . . . 8 (𝑥 = 𝑋 → (∃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
136129, 135rexeqbidv 3129 . . . . . . 7 (𝑥 = 𝑋 → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
137129, 136rexeqbidv 3129 . . . . . 6 (𝑥 = 𝑋 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
138137rspcev 3281 . . . . 5 ((𝑋𝑆 ∧ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄𝑔𝑄𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑))
13967, 128, 138syl2anc 690 . . . 4 ((((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) ∧ 𝜌) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑))
140139ex 448 . . 3 (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (𝜌 → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑)))
14166, 140impbid 200 . 2 (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜑) ↔ 𝜌))
14218, 141syl5bb 270 1 (((𝑋𝑆𝐴𝑄𝐵𝑄) ∧ (𝐶𝑄𝐷𝑄𝐸𝑄) ∧ (𝐹𝑄𝐺𝑄𝐻𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 194  wa 382  w3a 1030   = wceq 1474  wcel 1976  wrex 2896  cop 4130   class class class wbr 4577  {copab 4636
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4712  ax-pr 4828
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-eu 2461  df-mo 2462  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-ral 2900  df-rex 2901  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638
This theorem is referenced by:  brofs  31116  brifs  31154  brfs  31190
  Copyright terms: Public domain W3C validator