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

Theorem br8d 28636
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
StepHypRef Expression
1 br8d.10 . . . 4 (𝜑𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)})
21breqd 4588 . . 3 (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
3 opex 4853 . . . 4 ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∈ V
4 opex 4853 . . . 4 ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∈ V
5 eqeq1 2613 . . . . . . . . . 10 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
653anbi1d 1394 . . . . . . . . 9 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → ((𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
76rexbidv 3033 . . . . . . . 8 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
872rexbidv 3038 . . . . . . 7 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
982rexbidv 3038 . . . . . 6 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1092rexbidv 3038 . . . . 5 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1110rexbidv 3033 . . . 4 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
12 eqeq1 2613 . . . . . . . . . 10 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩))
13123anbi2d 1395 . . . . . . . . 9 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1413rexbidv 3033 . . . . . . . 8 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
15142rexbidv 3038 . . . . . . 7 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
16152rexbidv 3038 . . . . . 6 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
17162rexbidv 3038 . . . . 5 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1817rexbidv 3033 . . . 4 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
19 eqid 2609 . . . 4 {⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)} = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}
203, 4, 11, 18, 19brab 4913 . . 3 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
212, 20syl6bb 274 . 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 4853 . . . . . . . . . . . . . . 15 𝑎, 𝑏⟩ ∈ V
31 opex 4853 . . . . . . . . . . . . . . 15 𝑐, 𝑑⟩ ∈ V
3230, 31opth 4865 . . . . . . . . . . . . . 14 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ↔ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩))
33 vex 3175 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
34 vex 3175 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
3533, 34opth 4865 . . . . . . . . . . . . . . . 16 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐵))
36 br8d.1 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝐴 → (𝜓𝜒))
37 br8d.2 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝜒𝜃))
3836, 37sylan9bb 731 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝜓𝜃))
3935, 38sylbi 205 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜓𝜃))
40 vex 3175 . . . . . . . . . . . . . . . . 17 𝑐 ∈ V
41 vex 3175 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
4240, 41opth 4865 . . . . . . . . . . . . . . . 16 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶𝑑 = 𝐷))
43 br8d.3 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝐶 → (𝜃𝜏))
44 br8d.4 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝐷 → (𝜏𝜂))
4543, 44sylan9bb 731 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝜃𝜂))
4642, 45sylbi 205 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜃𝜂))
4739, 46sylan9bb 731 . . . . . . . . . . . . . 14 ((⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩) → (𝜓𝜂))
4832, 47sylbi 205 . . . . . . . . . . . . 13 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝜓𝜂))
4948eqcoms 2617 . . . . . . . . . . . 12 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ → (𝜓𝜂))
50 opex 4853 . . . . . . . . . . . . . . 15 𝑒, 𝑓⟩ ∈ V
51 opex 4853 . . . . . . . . . . . . . . 15 𝑔, ⟩ ∈ V
5250, 51opth 4865 . . . . . . . . . . . . . 14 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩))
53 vex 3175 . . . . . . . . . . . . . . . . 17 𝑒 ∈ V
54 vex 3175 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
5553, 54opth 4865 . . . . . . . . . . . . . . . 16 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
56 br8d.5 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝐸 → (𝜂𝜁))
57 br8d.6 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 → (𝜁𝜎))
5856, 57sylan9bb 731 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜂𝜎))
5955, 58sylbi 205 . . . . . . . . . . . . . . 15 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜂𝜎))
60 vex 3175 . . . . . . . . . . . . . . . . 17 𝑔 ∈ V
61 vex 3175 . . . . . . . . . . . . . . . . 17 ∈ V
6260, 61opth 4865 . . . . . . . . . . . . . . . 16 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ ↔ (𝑔 = 𝐺 = 𝐻))
63 br8d.7 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝐺 → (𝜎𝜌))
64 br8d.8 . . . . . . . . . . . . . . . . 17 ( = 𝐻 → (𝜌𝜇))
6563, 64sylan9bb 731 . . . . . . . . . . . . . . . 16 ((𝑔 = 𝐺 = 𝐻) → (𝜎𝜇))
6662, 65sylbi 205 . . . . . . . . . . . . . . 15 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ → (𝜎𝜇))
6759, 66sylan9bb 731 . . . . . . . . . . . . . 14 ((⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩) → (𝜂𝜇))
6852, 67sylbi 205 . . . . . . . . . . . . 13 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝜂𝜇))
6968eqcoms 2617 . . . . . . . . . . . 12 (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ → (𝜂𝜇))
7049, 69sylan9bb 731 . . . . . . . . . . 11 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩) → (𝜓𝜇))
7170biimp3a 1423 . . . . . . . . . 10 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇)
7271a1i 11 . . . . . . . . 9 ((((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) ∧ 𝑃) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7372rexlimdva 3012 . . . . . . . 8 (((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7473rexlimdvva 3019 . . . . . . 7 ((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7574rexlimdvva 3019 . . . . . 6 (((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7675rexlimdvva 3019 . . . . 5 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7776rexlimdva 3012 . . . 4 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
78 simpl1l 1104 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐴𝑃)
79 simpl1r 1105 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐵𝑃)
80 simpl21 1131 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐶𝑃)
81 simpl22 1132 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐷𝑃)
82 simpl23 1133 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐸𝑃)
83 simpl31 1134 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐹𝑃)
84 simpl32 1135 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐺𝑃)
85 simpl33 1136 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐻𝑃)
86 eqidd 2610 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
87 eqidd 2610 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
88 simpr 475 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝜇)
89 opeq1 4334 . . . . . . . . . . . 12 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
9089opeq2d 4341 . . . . . . . . . . 11 (𝑔 = 𝐺 → ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩)
9190eqeq2d 2619 . . . . . . . . . 10 (𝑔 = 𝐺 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩))
9291, 633anbi23d 1393 . . . . . . . . 9 (𝑔 = 𝐺 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜌)))
93 opeq2 4335 . . . . . . . . . . . 12 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
9493opeq2d 4341 . . . . . . . . . . 11 ( = 𝐻 → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
9594eqeq2d 2619 . . . . . . . . . 10 ( = 𝐻 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
9695, 643anbi23d 1393 . . . . . . . . 9 ( = 𝐻 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜌) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)))
9792, 96rspc2ev 3294 . . . . . . . 8 ((𝐺𝑃𝐻𝑃 ∧ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)) → ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎))
9884, 85, 86, 87, 88, 97syl113anc 1329 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎))
99 opeq2 4335 . . . . . . . . . . . 12 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
10099opeq2d 4341 . . . . . . . . . . 11 (𝑑 = 𝐷 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
101100eqeq2d 2619 . . . . . . . . . 10 (𝑑 = 𝐷 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
102101, 443anbi13d 1392 . . . . . . . . 9 (𝑑 = 𝐷 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
1031022rexbidv 3038 . . . . . . . 8 (𝑑 = 𝐷 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
104 opeq1 4334 . . . . . . . . . . . 12 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
105104opeq1d 4340 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩)
106105eqeq2d 2619 . . . . . . . . . 10 (𝑒 = 𝐸 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩))
107106, 563anbi23d 1393 . . . . . . . . 9 (𝑒 = 𝐸 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
1081072rexbidv 3038 . . . . . . . 8 (𝑒 = 𝐸 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
109 opeq2 4335 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
110109opeq1d 4340 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩)
111110eqeq2d 2619 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩))
112111, 573anbi23d 1393 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)))
1131122rexbidv 3038 . . . . . . . 8 (𝑓 = 𝐹 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)))
114103, 108, 113rspc3ev 3296 . . . . . . 7 (((𝐷𝑃𝐸𝑃𝐹𝑃) ∧ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)) → ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏))
11581, 82, 83, 98, 114syl31anc 1320 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏))
116 opeq1 4334 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
117116opeq1d 4340 . . . . . . . . . . . 12 (𝑎 = 𝐴 → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
118117eqeq2d 2619 . . . . . . . . . . 11 (𝑎 = 𝐴 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
119118, 363anbi13d 1392 . . . . . . . . . 10 (𝑎 = 𝐴 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
120119rexbidv 3033 . . . . . . . . 9 (𝑎 = 𝐴 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1211202rexbidv 3038 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1221212rexbidv 3038 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
123 opeq2 4335 . . . . . . . . . . . . 13 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
124123opeq1d 4340 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩)
125124eqeq2d 2619 . . . . . . . . . . 11 (𝑏 = 𝐵 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩))
126125, 373anbi13d 1392 . . . . . . . . . 10 (𝑏 = 𝐵 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
127126rexbidv 3033 . . . . . . . . 9 (𝑏 = 𝐵 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1281272rexbidv 3038 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1291282rexbidv 3038 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
130 opeq1 4334 . . . . . . . . . . . . 13 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
131130opeq2d 4341 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩)
132131eqeq2d 2619 . . . . . . . . . . 11 (𝑐 = 𝐶 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩))
133132, 433anbi13d 1392 . . . . . . . . . 10 (𝑐 = 𝐶 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
134133rexbidv 3033 . . . . . . . . 9 (𝑐 = 𝐶 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
1351342rexbidv 3038 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
1361352rexbidv 3038 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
137122, 129, 136rspc3ev 3296 . . . . . 6 (((𝐴𝑃𝐵𝑃𝐶𝑃) ∧ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
13878, 79, 80, 115, 137syl31anc 1320 . . . . 5 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
139138ex 448 . . . 4 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (𝜇 → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
14077, 139impbid 200 . . 3 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ 𝜇))
14122, 23, 24, 25, 26, 27, 28, 29, 140syl233anc 1346 . 2 (𝜑 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ 𝜇))
14221, 141bitrd 266 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:  brafs  29837
  Copyright terms: Public domain W3C validator