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 33720
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 5383 . . 3 𝐴, ⟨𝐵, 𝐶⟩⟩ ∈ V
2 opex 5383 . . 3 𝐷, ⟨𝐸, 𝐹⟩⟩ ∈ V
3 eqeq1 2744 . . . . . . . . 9 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩))
4 eqcom 2747 . . . . . . . . 9 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
53, 4bitrdi 287 . . . . . . . 8 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ↔ ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
653anbi1d 1439 . . . . . . 7 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → ((𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
76rexbidv 3228 . . . . . 6 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
872rexbidv 3231 . . . . 5 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
982rexbidv 3231 . . . 4 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
1092rexbidv 3231 . . 3 (𝑝 = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)))
11 eqeq1 2744 . . . . . . . . 9 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩))
12 eqcom 2747 . . . . . . . . 9 (⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
1311, 12bitrdi 287 . . . . . . . 8 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ↔ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
14133anbi2d 1440 . . . . . . 7 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
1514rexbidv 3228 . . . . . 6 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
16152rexbidv 3231 . . . . 5 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
17162rexbidv 3231 . . . 4 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
18172rexbidv 3231 . . 3 (𝑞 = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑) ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
19 br6.8 . . 3 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (𝑝 = ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ ∧ 𝑞 = ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ ∧ 𝜑)}
201, 2, 10, 18, 19brab 5459 . 2 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
21 vex 3435 . . . . . . . . . . . 12 𝑎 ∈ V
22 opex 5383 . . . . . . . . . . . 12 𝑏, 𝑐⟩ ∈ V
2321, 22opth 5395 . . . . . . . . . . 11 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ (𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩))
24 br6.1 . . . . . . . . . . . 12 (𝑎 = 𝐴 → (𝜑𝜓))
25 vex 3435 . . . . . . . . . . . . . 14 𝑏 ∈ V
26 vex 3435 . . . . . . . . . . . . . 14 𝑐 ∈ V
2725, 26opth 5395 . . . . . . . . . . . . 13 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ ↔ (𝑏 = 𝐵𝑐 = 𝐶))
28 br6.2 . . . . . . . . . . . . . 14 (𝑏 = 𝐵 → (𝜓𝜒))
29 br6.3 . . . . . . . . . . . . . 14 (𝑐 = 𝐶 → (𝜒𝜃))
3028, 29sylan9bb 510 . . . . . . . . . . . . 13 ((𝑏 = 𝐵𝑐 = 𝐶) → (𝜓𝜃))
3127, 30sylbi 216 . . . . . . . . . . . 12 (⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩ → (𝜓𝜃))
3224, 31sylan9bb 510 . . . . . . . . . . 11 ((𝑎 = 𝐴 ∧ ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝐶⟩) → (𝜑𝜃))
3323, 32sylbi 216 . . . . . . . . . 10 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ → (𝜑𝜃))
34 vex 3435 . . . . . . . . . . . 12 𝑑 ∈ V
35 opex 5383 . . . . . . . . . . . 12 𝑒, 𝑓⟩ ∈ V
3634, 35opth 5395 . . . . . . . . . . 11 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ (𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩))
37 br6.4 . . . . . . . . . . . 12 (𝑑 = 𝐷 → (𝜃𝜏))
38 vex 3435 . . . . . . . . . . . . . 14 𝑒 ∈ V
39 vex 3435 . . . . . . . . . . . . . 14 𝑓 ∈ V
4038, 39opth 5395 . . . . . . . . . . . . 13 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸𝑓 = 𝐹))
41 br6.5 . . . . . . . . . . . . . 14 (𝑒 = 𝐸 → (𝜏𝜂))
42 br6.6 . . . . . . . . . . . . . 14 (𝑓 = 𝐹 → (𝜂𝜁))
4341, 42sylan9bb 510 . . . . . . . . . . . . 13 ((𝑒 = 𝐸𝑓 = 𝐹) → (𝜏𝜁))
4440, 43sylbi 216 . . . . . . . . . . . 12 (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏𝜁))
4537, 44sylan9bb 510 . . . . . . . . . . 11 ((𝑑 = 𝐷 ∧ ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩) → (𝜃𝜁))
4636, 45sylbi 216 . . . . . . . . . 10 (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ → (𝜃𝜁))
4733, 46sylan9bb 510 . . . . . . . . 9 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) → (𝜑𝜁))
4847biimp3a 1468 . . . . . . . 8 ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁)
4948a1i 11 . . . . . . 7 ((((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) ∧ 𝑓𝑃) → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5049rexlimdva 3215 . . . . . 6 (((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) ∧ (𝑑𝑃𝑒𝑃)) → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5150rexlimdvva 3225 . . . . 5 ((((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) ∧ (𝑏𝑃𝑐𝑃)) → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5251rexlimdvva 3225 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ (𝑥𝑆𝑎𝑃)) → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
5352rexlimdvva 3225 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) → 𝜁))
54 simpl1 1190 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → 𝑋𝑆)
55 simpl2 1191 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → (𝐴𝑄𝐵𝑄𝐶𝑄))
56 opeq1 4810 . . . . . . . . . 10 (𝑑 = 𝐷 → ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝑒, 𝑓⟩⟩)
5756eqeq1d 2742 . . . . . . . . 9 (𝑑 = 𝐷 → (⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
5857, 373anbi23d 1438 . . . . . . . 8 (𝑑 = 𝐷 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏)))
59 opeq1 4810 . . . . . . . . . . 11 (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩)
6059opeq2d 4817 . . . . . . . . . 10 (𝑒 = 𝐸 → ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝑓⟩⟩)
6160eqeq1d 2742 . . . . . . . . 9 (𝑒 = 𝐸 → (⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6261, 413anbi23d 1438 . . . . . . . 8 (𝑒 = 𝐸 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜏) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂)))
63 opeq2 4811 . . . . . . . . . . . 12 (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩)
6463opeq2d 4817 . . . . . . . . . . 11 (𝑓 = 𝐹 → ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
6564eqeq1d 2742 . . . . . . . . . 10 (𝑓 = 𝐹 → (⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩))
6665, 423anbi23d 1438 . . . . . . . . 9 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁)))
67 eqid 2740 . . . . . . . . . . 11 𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩
68 eqid 2740 . . . . . . . . . . 11 𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩
6967, 68pm3.2i 471 . . . . . . . . . 10 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩)
70 df-3an 1088 . . . . . . . . . 10 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩) ∧ 𝜁))
7169, 70mpbiran 706 . . . . . . . . 9 ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜁) ↔ 𝜁)
7266, 71bitrdi 287 . . . . . . . 8 (𝑓 = 𝐹 → ((⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝐷, ⟨𝐸, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜂) ↔ 𝜁))
7358, 62, 72rspc3ev 3575 . . . . . . 7 (((𝐷𝑄𝐸𝑄𝐹𝑄) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
74733ad2antl3 1186 . . . . . 6 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃))
75 opeq1 4810 . . . . . . . . . . 11 (𝑎 = 𝐴 → ⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝑏, 𝑐⟩⟩)
7675eqeq1d 2742 . . . . . . . . . 10 (𝑎 = 𝐴 → (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
7776, 243anbi13d 1437 . . . . . . . . 9 (𝑎 = 𝐴 → ((⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
7877rexbidv 3228 . . . . . . . 8 (𝑎 = 𝐴 → (∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
79782rexbidv 3231 . . . . . . 7 (𝑎 = 𝐴 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓)))
80 opeq1 4810 . . . . . . . . . . . 12 (𝑏 = 𝐵 → ⟨𝑏, 𝑐⟩ = ⟨𝐵, 𝑐⟩)
8180opeq2d 4817 . . . . . . . . . . 11 (𝑏 = 𝐵 → ⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝑐⟩⟩)
8281eqeq1d 2742 . . . . . . . . . 10 (𝑏 = 𝐵 → (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8382, 283anbi13d 1437 . . . . . . . . 9 (𝑏 = 𝐵 → ((⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
8483rexbidv 3228 . . . . . . . 8 (𝑏 = 𝐵 → (∃𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
85842rexbidv 3231 . . . . . . 7 (𝑏 = 𝐵 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜓) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒)))
86 opeq2 4811 . . . . . . . . . . . 12 (𝑐 = 𝐶 → ⟨𝐵, 𝑐⟩ = ⟨𝐵, 𝐶⟩)
8786opeq2d 4817 . . . . . . . . . . 11 (𝑐 = 𝐶 → ⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩)
8887eqeq1d 2742 . . . . . . . . . 10 (𝑐 = 𝐶 → (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ↔ ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩))
8988, 293anbi13d 1437 . . . . . . . . 9 (𝑐 = 𝐶 → ((⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9089rexbidv 3228 . . . . . . . 8 (𝑐 = 𝐶 → (∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
91902rexbidv 3231 . . . . . . 7 (𝑐 = 𝐶 → (∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜒) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)))
9279, 85, 91rspc3ev 3575 . . . . . 6 (((𝐴𝑄𝐵𝑄𝐶𝑄) ∧ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝐴, ⟨𝐵, 𝐶⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜃)) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
9355, 74, 92syl2anc 584 . . . . 5 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
94 br6.7 . . . . . . 7 (𝑥 = 𝑋𝑃 = 𝑄)
9594rexeqdv 3348 . . . . . . . . . . 11 (𝑥 = 𝑋 → (∃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9694, 95rexeqbidv 3336 . . . . . . . . . 10 (𝑥 = 𝑋 → (∃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9794, 96rexeqbidv 3336 . . . . . . . . 9 (𝑥 = 𝑋 → (∃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9894, 97rexeqbidv 3336 . . . . . . . 8 (𝑥 = 𝑋 → (∃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
9994, 98rexeqbidv 3336 . . . . . . 7 (𝑥 = 𝑋 → (∃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10094, 99rexeqbidv 3336 . . . . . 6 (𝑥 = 𝑋 → (∃𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
101100rspcev 3561 . . . . 5 ((𝑋𝑆 ∧ ∃𝑎𝑄𝑏𝑄𝑐𝑄𝑑𝑄𝑒𝑄𝑓𝑄 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
10254, 93, 101syl2anc 584 . . . 4 (((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) ∧ 𝜁) → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑))
103102ex 413 . . 3 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (𝜁 → ∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑)))
10453, 103impbid 211 . 2 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (∃𝑥𝑆𝑎𝑃𝑏𝑃𝑐𝑃𝑑𝑃𝑒𝑃𝑓𝑃 (⟨𝑎, ⟨𝑏, 𝑐⟩⟩ = ⟨𝐴, ⟨𝐵, 𝐶⟩⟩ ∧ ⟨𝑑, ⟨𝑒, 𝑓⟩⟩ = ⟨𝐷, ⟨𝐸, 𝐹⟩⟩ ∧ 𝜑) ↔ 𝜁))
10520, 104syl5bb 283 1 ((𝑋𝑆 ∧ (𝐴𝑄𝐵𝑄𝐶𝑄) ∧ (𝐷𝑄𝐸𝑄𝐹𝑄)) → (⟨𝐴, ⟨𝐵, 𝐶⟩⟩𝑅𝐷, ⟨𝐸, 𝐹⟩⟩ ↔ 𝜁))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 396  w3a 1086   = wceq 1542  wcel 2110  wrex 3067  cop 4573   class class class wbr 5079  {copab 5141
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2015  ax-8 2112  ax-9 2120  ax-ext 2711  ax-sep 5227  ax-nul 5234  ax-pr 5356
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1545  df-fal 1555  df-ex 1787  df-sb 2072  df-clab 2718  df-cleq 2732  df-clel 2818  df-ral 3071  df-rex 3072  df-rab 3075  df-v 3433  df-dif 3895  df-un 3897  df-nul 4263  df-if 4466  df-sn 4568  df-pr 4570  df-op 4574  df-br 5080  df-opab 5142
This theorem is referenced by:  brcgr3  34344
  Copyright terms: Public domain W3C validator