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

Theorem br6 31352
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
StepHypRef Expression
1 opex 4893 . . 3 𝐴, ⟨𝐵, 𝐶⟩⟩ ∈ V
2 opex 4893 . . 3 𝐷, ⟨𝐸, 𝐹⟩⟩ ∈ V
3 eqeq1 2625 . . . . . . . . 9 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩))
4 eqcom 2628 . . . . . . . . 9 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
53, 4syl6bb 276 . . . . . . . 8 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
653anbi1d 1400 . . . . . . 7 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → ((𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
76rexbidv 3045 . . . . . 6 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
872rexbidv 3050 . . . . 5 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
982rexbidv 3050 . . . 4 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
1092rexbidv 3050 . . 3 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
11 eqeq1 2625 . . . . . . . . 9 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩))
12 eqcom 2628 . . . . . . . . 9 (⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
1311, 12syl6bb 276 . . . . . . . 8 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
14133anbi2d 1401 . . . . . . 7 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
1514rexbidv 3045 . . . . . 6 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
16152rexbidv 3050 . . . . 5 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
17162rexbidv 3050 . . . 4 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
18172rexbidv 3050 . . 3 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
19 br6.8 . . 3 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
201, 2, 10, 18, 19brab 4958 . 2 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
21 vex 3189 . . . . . . . . . . . 12 𝑎 ∈ V
22 opex 4893 . . . . . . . . . . . 12 𝑏, 𝑐⟩ ∈ V
2321, 22opth 4905 . . . . . . . . . . 11 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ (𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩))
24 br6.1 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (𝜑𝜓))
25 vex 3189 . . . . . . . . . . . . . 14 𝑏 ∈ V
26 vex 3189 . . . . . . . . . . . . . 14 𝑐 ∈ V
2725, 26opth 4905 . . . . . . . . . . . . 13 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ ↔ (𝑏 = 𝐵𝑐 = 𝐶))
28 br6.2 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (𝜓𝜒))
29 br6.3 . . . . . . . . . . . . . 14 (𝑐 = 𝐶 → (𝜒𝜃))
3028, 29sylan9bb 735 . . . . . . . . . . . . 13 ((𝑏 = 𝐵𝑐 = 𝐶) → (𝜓𝜃))
3127, 30sylbi 207 . . . . . . . . . . . 12 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ → (𝜓𝜃))
3224, 31sylan9bb 735 . . . . . . . . . . 11 ((𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩) → (𝜑𝜃))
3323, 32sylbi 207 . . . . . . . . . 10 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝜑𝜃))
34 vex 3189 . . . . . . . . . . . 12 𝑑 ∈ V
35 opex 4893 . . . . . . . . . . . 12 𝑒, 𝑓⟩ ∈ V
3634, 35opth 4905 . . . . . . . . . . 11 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩))
37 br6.4 . . . . . . . . . . . 12 (𝑑 = 𝐷 → (𝜃𝜏))
38 vex 3189 . . . . . . . . . . . . . 14 𝑒 ∈ V
39 vex 3189 . . . . . . . . . . . . . 14 𝑓 ∈ V
4038, 39opth 4905 . . . . . . . . . . . . 13 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
41 br6.5 . . . . . . . . . . . . . 14 (𝑒 = 𝐸 → (𝜏𝜂))
42 br6.6 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → (𝜂𝜁))
4341, 42sylan9bb 735 . . . . . . . . . . . . 13 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜏𝜁))
4440, 43sylbi 207 . . . . . . . . . . . 12 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏𝜁))
4537, 44sylan9bb 735 . . . . . . . . . . 11 ((𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩) → (𝜃𝜁))
4636, 45sylbi 207 . . . . . . . . . 10 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝜃𝜁))
4733, 46sylan9bb 735 . . . . . . . . 9 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) → (𝜑𝜁))
4847biimp3a 1429 . . . . . . . 8 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁)
4948a1i 11 . . . . . . 7 ((((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ 𝑓𝑃) → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5049rexlimdva 3024 . . . . . 6 (((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5150rexlimdvva 3031 . . . . 5 ((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5251rexlimdvva 3031 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5352rexlimdvva 3031 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
54 simpl1 1062 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → 𝑋𝑆)
55 simpl2 1063 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → (𝐴𝑄𝐵𝑄𝐶𝑄))
56 opeq1 4370 . . . . . . . . . 10 (𝑑 = 𝐷 → ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝑒, 𝑓⟩⟩)
5756eqeq1d 2623 . . . . . . . . 9 (𝑑 = 𝐷 → (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
5857, 373anbi23d 1399 . . . . . . . 8 (𝑑 = 𝐷 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏)))
59 opeq1 4370 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
6059opeq2d 4377 . . . . . . . . . 10 (𝑒 = 𝐸 → ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝑓⟩⟩)
6160eqeq1d 2623 . . . . . . . . 9 (𝑒 = 𝐸 → (⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6261, 413anbi23d 1399 . . . . . . . 8 (𝑒 = 𝐸 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂)))
63 opeq2 4371 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
6463opeq2d 4377 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
6564eqeq1d 2623 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6665, 423anbi23d 1399 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁)))
67 eqid 2621 . . . . . . . . . . 11 𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩
68 eqid 2621 . . . . . . . . . . 11 𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩
6967, 68pm3.2i 471 . . . . . . . . . 10 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
70 df-3an 1038 . . . . . . . . . 10 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) ∧ 𝜁))
7169, 70mpbiran 952 . . . . . . . . 9 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ 𝜁)
7266, 71syl6bb 276 . . . . . . . 8 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ 𝜁))
7358, 62, 72rspc3ev 3310 . . . . . . 7 (((𝐷𝑄𝐸𝑄𝐹𝑄) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
74733ad2antl3 1223 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
75 opeq1 4370 . . . . . . . . . . 11 (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
7675eqeq1d 2623 . . . . . . . . . 10 (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
7776, 243anbi13d 1398 . . . . . . . . 9 (𝑎 = 𝐴 → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
7877rexbidv 3045 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
79782rexbidv 3050 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
80 opeq1 4370 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
8180opeq2d 4377 . . . . . . . . . . 11 (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
8281eqeq1d 2623 . . . . . . . . . 10 (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8382, 283anbi13d 1398 . . . . . . . . 9 (𝑏 = 𝐵 → ((⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
8483rexbidv 3045 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
85842rexbidv 3050 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
86 opeq2 4371 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
8786opeq2d 4377 . . . . . . . . . . 11 (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
8887eqeq1d 2623 . . . . . . . . . 10 (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8988, 293anbi13d 1398 . . . . . . . . 9 (𝑐 = 𝐶 → ((⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9089rexbidv 3045 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
91902rexbidv 3050 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9279, 85, 91rspc3ev 3310 . . . . . 6 (((𝐴𝑄𝐵𝑄𝐶𝑄) ∧ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
9355, 74, 92syl2anc 692 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
94 br6.7 . . . . . . 7 (𝑥 = 𝑋𝑃 = 𝑄)
9594rexeqdv 3134 . . . . . . . . . . 11 (𝑥 = 𝑋 → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9694, 95rexeqbidv 3142 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9794, 96rexeqbidv 3142 . . . . . . . . 9 (𝑥 = 𝑋 → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9894, 97rexeqbidv 3142 . . . . . . . 8 (𝑥 = 𝑋 → (∃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9994, 98rexeqbidv 3142 . . . . . . 7 (𝑥 = 𝑋 → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10094, 99rexeqbidv 3142 . . . . . 6 (𝑥 = 𝑋 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
101100rspcev 3295 . . . . 5 ((𝑋𝑆 ∧ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
10254, 93, 101syl2anc 692 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
103102ex 450 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (𝜁 → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10453, 103impbid 202 . 2 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ 𝜁))
10520, 104syl5bb 272 1 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 384  w3a 1036   = wceq 1480  wcel 1987  wrex 2908  cop 4154   class class class wbr 4613  {copab 4672
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601  ax-sep 4741  ax-nul 4749  ax-pr 4867
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-eu 2473  df-mo 2474  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-ral 2912  df-rex 2913  df-rab 2916  df-v 3188  df-dif 3558  df-un 3560  df-in 3562  df-ss 3569  df-nul 3892  df-if 4059  df-sn 4149  df-pr 4151  df-op 4155  df-br 4614  df-opab 4674
This theorem is referenced by:  brcgr3  31792
  Copyright terms: Public domain W3C validator