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 29747
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 4855 . . 3 (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
3 opex 5122 . . . 4 ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∈ V
4 opex 5122 . . . 4 ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∈ V
5 eqeq1 2810 . . . . . . . . . 10 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
653anbi1d 1557 . . . . . . . . 9 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → ((𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
76rexbidv 3240 . . . . . . . 8 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
872rexbidv 3245 . . . . . . 7 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
982rexbidv 3245 . . . . . 6 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1092rexbidv 3245 . . . . 5 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1110rexbidv 3240 . . . 4 (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
12 eqeq1 2810 . . . . . . . . . 10 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩))
13123anbi2d 1558 . . . . . . . . 9 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1413rexbidv 3240 . . . . . . . 8 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
15142rexbidv 3245 . . . . . . 7 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
16152rexbidv 3245 . . . . . 6 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
17162rexbidv 3245 . . . . 5 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
1817rexbidv 3240 . . . 4 (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
19 eqid 2806 . . . 4 {⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)} = {⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}
203, 4, 11, 18, 19brab 5193 . . 3 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩{⟨𝑝, 𝑞⟩ ∣ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)}⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
212, 20syl6bb 278 . 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 5122 . . . . . . . . . . . . . . 15 𝑎, 𝑏⟩ ∈ V
31 opex 5122 . . . . . . . . . . . . . . 15 𝑐, 𝑑⟩ ∈ V
3230, 31opth 5134 . . . . . . . . . . . . . 14 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ↔ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩))
33 vex 3394 . . . . . . . . . . . . . . . . 17 𝑎 ∈ V
34 vex 3394 . . . . . . . . . . . . . . . . 17 𝑏 ∈ V
3533, 34opth 5134 . . . . . . . . . . . . . . . 16 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴𝑏 = 𝐵))
36 br8d.1 . . . . . . . . . . . . . . . . 17 (𝑎 = 𝐴 → (𝜓𝜒))
37 br8d.2 . . . . . . . . . . . . . . . . 17 (𝑏 = 𝐵 → (𝜒𝜃))
3836, 37sylan9bb 501 . . . . . . . . . . . . . . . 16 ((𝑎 = 𝐴𝑏 = 𝐵) → (𝜓𝜃))
3935, 38sylbi 208 . . . . . . . . . . . . . . 15 (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜓𝜃))
40 vex 3394 . . . . . . . . . . . . . . . . 17 𝑐 ∈ V
41 vex 3394 . . . . . . . . . . . . . . . . 17 𝑑 ∈ V
4240, 41opth 5134 . . . . . . . . . . . . . . . 16 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶𝑑 = 𝐷))
43 br8d.3 . . . . . . . . . . . . . . . . 17 (𝑐 = 𝐶 → (𝜃𝜏))
44 br8d.4 . . . . . . . . . . . . . . . . 17 (𝑑 = 𝐷 → (𝜏𝜂))
4543, 44sylan9bb 501 . . . . . . . . . . . . . . . 16 ((𝑐 = 𝐶𝑑 = 𝐷) → (𝜃𝜂))
4642, 45sylbi 208 . . . . . . . . . . . . . . 15 (⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜃𝜂))
4739, 46sylan9bb 501 . . . . . . . . . . . . . 14 ((⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩) → (𝜓𝜂))
4832, 47sylbi 208 . . . . . . . . . . . . 13 (⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝜓𝜂))
4948eqcoms 2814 . . . . . . . . . . . 12 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ → (𝜓𝜂))
50 opex 5122 . . . . . . . . . . . . . . 15 𝑒, 𝑓⟩ ∈ V
51 opex 5122 . . . . . . . . . . . . . . 15 𝑔, ⟩ ∈ V
5250, 51opth 5134 . . . . . . . . . . . . . 14 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩))
53 vex 3394 . . . . . . . . . . . . . . . . 17 𝑒 ∈ V
54 vex 3394 . . . . . . . . . . . . . . . . 17 𝑓 ∈ V
5553, 54opth 5134 . . . . . . . . . . . . . . . 16 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
56 br8d.5 . . . . . . . . . . . . . . . . 17 (𝑒 = 𝐸 → (𝜂𝜁))
57 br8d.6 . . . . . . . . . . . . . . . . 17 (𝑓 = 𝐹 → (𝜁𝜎))
5856, 57sylan9bb 501 . . . . . . . . . . . . . . . 16 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜂𝜎))
5955, 58sylbi 208 . . . . . . . . . . . . . . 15 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜂𝜎))
60 vex 3394 . . . . . . . . . . . . . . . . 17 𝑔 ∈ V
61 vex 3394 . . . . . . . . . . . . . . . . 17 ∈ V
6260, 61opth 5134 . . . . . . . . . . . . . . . 16 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ ↔ (𝑔 = 𝐺 = 𝐻))
63 br8d.7 . . . . . . . . . . . . . . . . 17 (𝑔 = 𝐺 → (𝜎𝜌))
64 br8d.8 . . . . . . . . . . . . . . . . 17 ( = 𝐻 → (𝜌𝜇))
6563, 64sylan9bb 501 . . . . . . . . . . . . . . . 16 ((𝑔 = 𝐺 = 𝐻) → (𝜎𝜇))
6662, 65sylbi 208 . . . . . . . . . . . . . . 15 (⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩ → (𝜎𝜇))
6759, 66sylan9bb 501 . . . . . . . . . . . . . 14 ((⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ⟩ = ⟨𝐺, 𝐻⟩) → (𝜂𝜇))
6852, 67sylbi 208 . . . . . . . . . . . . 13 (⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝜂𝜇))
6968eqcoms 2814 . . . . . . . . . . . 12 (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ → (𝜂𝜇))
7049, 69sylan9bb 501 . . . . . . . . . . 11 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩) → (𝜓𝜇))
7170biimp3a 1586 . . . . . . . . . 10 ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇)
7271a1i 11 . . . . . . . . 9 ((((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) ∧ 𝑃) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7372rexlimdva 3219 . . . . . . . 8 (((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ (𝑓𝑃𝑔𝑃)) → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7473rexlimdvva 3226 . . . . . . 7 ((((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7574rexlimdvva 3226 . . . . . 6 (((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7675rexlimdvva 3226 . . . . 5 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝑎𝑃) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
7776rexlimdva 3219 . . . 4 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) → 𝜇))
78 simpl1l 1286 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐴𝑃)
79 simpl1r 1288 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐵𝑃)
80 simpl21 1328 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐶𝑃)
81 simpl22 1330 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐷𝑃)
82 simpl23 1332 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐸𝑃)
83 simpl31 1334 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐹𝑃)
84 simpl32 1336 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐺𝑃)
85 simpl33 1338 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝐻𝑃)
86 eqidd 2807 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
87 eqidd 2807 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
88 simpr 473 . . . . . . . 8 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → 𝜇)
89 opeq1 4595 . . . . . . . . . . . 12 (𝑔 = 𝐺 → ⟨𝑔, ⟩ = ⟨𝐺, ⟩)
9089opeq2d 4602 . . . . . . . . . . 11 (𝑔 = 𝐺 → ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩)
9190eqeq2d 2816 . . . . . . . . . 10 (𝑔 = 𝐺 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩))
9291, 633anbi23d 1556 . . . . . . . . 9 (𝑔 = 𝐺 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜌)))
93 opeq2 4596 . . . . . . . . . . . 12 ( = 𝐻 → ⟨𝐺, ⟩ = ⟨𝐺, 𝐻⟩)
9493opeq2d 4602 . . . . . . . . . . 11 ( = 𝐻 → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)
9594eqeq2d 2816 . . . . . . . . . 10 ( = 𝐻 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩))
9695, 643anbi23d 1556 . . . . . . . . 9 ( = 𝐻 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ⟩⟩ ∧ 𝜌) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)))
9792, 96rspc2ev 3517 . . . . . . . 8 ((𝐺𝑃𝐻𝑃 ∧ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜇)) → ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎))
9884, 85, 86, 87, 88, 97syl113anc 1494 . . . . . . 7 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎))
99 opeq2 4596 . . . . . . . . . . . 12 (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩)
10099opeq2d 4602 . . . . . . . . . . 11 (𝑑 = 𝐷 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)
101100eqeq2d 2816 . . . . . . . . . 10 (𝑑 = 𝐷 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩))
102101, 443anbi13d 1555 . . . . . . . . 9 (𝑑 = 𝐷 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
1031022rexbidv 3245 . . . . . . . 8 (𝑑 = 𝐷 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂)))
104 opeq1 4595 . . . . . . . . . . . 12 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
105104opeq1d 4601 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩)
106105eqeq2d 2816 . . . . . . . . . 10 (𝑒 = 𝐸 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩))
107106, 563anbi23d 1556 . . . . . . . . 9 (𝑒 = 𝐸 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
1081072rexbidv 3245 . . . . . . . 8 (𝑒 = 𝐸 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜂) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁)))
109 opeq2 4596 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
110109opeq1d 4601 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩)
111110eqeq2d 2816 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩))
112111, 573anbi23d 1556 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)))
1131122rexbidv 3245 . . . . . . . 8 (𝑓 = 𝐹 → (∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜁) ↔ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)))
114103, 108, 113rspc3ev 3519 . . . . . . 7 (((𝐷𝑃𝐸𝑃𝐹𝑃) ∧ ∃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ⟩⟩ ∧ 𝜎)) → ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏))
11581, 82, 83, 98, 114syl31anc 1485 . . . . . 6 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏))
116 opeq1 4595 . . . . . . . . . . . . 13 (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩)
117116opeq1d 4601 . . . . . . . . . . . 12 (𝑎 = 𝐴 → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)
118117eqeq2d 2816 . . . . . . . . . . 11 (𝑎 = 𝐴 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩))
119118, 363anbi13d 1555 . . . . . . . . . 10 (𝑎 = 𝐴 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
120119rexbidv 3240 . . . . . . . . 9 (𝑎 = 𝐴 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1211202rexbidv 3245 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
1221212rexbidv 3245 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒)))
123 opeq2 4596 . . . . . . . . . . . . 13 (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩)
124123opeq1d 4601 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩)
125124eqeq2d 2816 . . . . . . . . . . 11 (𝑏 = 𝐵 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩))
126125, 373anbi13d 1555 . . . . . . . . . 10 (𝑏 = 𝐵 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
127126rexbidv 3240 . . . . . . . . 9 (𝑏 = 𝐵 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1281272rexbidv 3245 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
1291282rexbidv 3245 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃)))
130 opeq1 4595 . . . . . . . . . . . . 13 (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩)
131130opeq2d 4602 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩)
132131eqeq2d 2816 . . . . . . . . . . 11 (𝑐 = 𝐶 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩))
133132, 433anbi13d 1555 . . . . . . . . . 10 (𝑐 = 𝐶 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
134133rexbidv 3240 . . . . . . . . 9 (𝑐 = 𝐶 → (∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
1351342rexbidv 3245 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
1361352rexbidv 3245 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜃) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)))
137122, 129, 136rspc3ev 3519 . . . . . 6 (((𝐴𝑃𝐵𝑃𝐶𝑃) ∧ ∃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜏)) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
13878, 79, 80, 115, 137syl31anc 1485 . . . . 5 ((((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) ∧ 𝜇) → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓))
139138ex 399 . . . 4 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (𝜇 → ∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓)))
14077, 139impbid 203 . . 3 (((𝐴𝑃𝐵𝑃) ∧ (𝐶𝑃𝐷𝑃𝐸𝑃) ∧ (𝐹𝑃𝐺𝑃𝐻𝑃)) → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ 𝜇))
14122, 23, 24, 25, 26, 27, 28, 29, 140syl233anc 1511 . 2 (𝜑 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃𝑔𝑃𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ⟩⟩ ∧ 𝜓) ↔ 𝜇))
14221, 141bitrd 270 1 (𝜑 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜇))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 197  wa 384  w3a 1100   = wceq 1637  wcel 2156  wrex 3097  cop 4376   class class class wbr 4844  {copab 4906
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784  ax-sep 4975  ax-nul 4983  ax-pr 5096
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-eu 2634  df-mo 2635  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-ral 3101  df-rex 3102  df-rab 3105  df-v 3393  df-dif 3772  df-un 3774  df-in 3776  df-ss 3783  df-nul 4117  df-if 4280  df-sn 4371  df-pr 4373  df-op 4377  df-br 4845  df-opab 4907
This theorem is referenced by:  brafs  31075
  Copyright terms: Public domain W3C validator