Step | Hyp | Ref
| Expression |
1 | | opex 5426 |
. . 3
⊢
⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∈ V |
2 | | opex 5426 |
. . 3
⊢
⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∈ V |
3 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)) |
4 | 3 | 3anbi1d 1441 |
. . . . . . . 8
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → ((𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
5 | 4 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
6 | 5 | 2rexbidv 3214 |
. . . . . 6
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
7 | 6 | 2rexbidv 3214 |
. . . . 5
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
8 | 7 | 2rexbidv 3214 |
. . . 4
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
9 | 8 | 2rexbidv 3214 |
. . 3
⊢ (𝑝 = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
10 | | eqeq1 2741 |
. . . . . . . . 9
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩)) |
11 | 10 | 3anbi2d 1442 |
. . . . . . . 8
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
12 | 11 | rexbidv 3176 |
. . . . . . 7
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
13 | 12 | 2rexbidv 3214 |
. . . . . 6
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
14 | 13 | 2rexbidv 3214 |
. . . . 5
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
15 | 14 | 2rexbidv 3214 |
. . . 4
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
16 | 15 | 2rexbidv 3214 |
. . 3
⊢ (𝑞 = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
17 | | br8.10 |
. . 3
⊢ 𝑅 = {⟨𝑝, 𝑞⟩ ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ 𝑞 = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)} |
18 | 1, 2, 9, 16, 17 | brab 5505 |
. 2
⊢
(⟨⟨𝐴,
𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) |
19 | | opex 5426 |
. . . . . . . . . . . . . 14
⊢
⟨𝑎, 𝑏⟩ ∈ V |
20 | | opex 5426 |
. . . . . . . . . . . . . 14
⊢
⟨𝑐, 𝑑⟩ ∈ V |
21 | 19, 20 | opth 5438 |
. . . . . . . . . . . . 13
⊢
(⟨⟨𝑎,
𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ↔ (⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩)) |
22 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑎 ∈ V |
23 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
24 | 22, 23 | opth 5438 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) |
25 | | br8.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) |
26 | | br8.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) |
27 | 25, 26 | sylan9bb 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒)) |
28 | 24, 27 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ → (𝜑 ↔ 𝜒)) |
29 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
30 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑑 ∈ V |
31 | 29, 30 | opth 5438 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) |
32 | | br8.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) |
33 | | br8.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) |
34 | 32, 33 | sylan9bb 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏)) |
35 | 31, 34 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩ → (𝜒 ↔ 𝜏)) |
36 | 28, 35 | sylan9bb 511 |
. . . . . . . . . . . . 13
⊢
((⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝐵⟩ ∧ ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝐷⟩) → (𝜑 ↔ 𝜏)) |
37 | 21, 36 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(⟨⟨𝑎,
𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ → (𝜑 ↔ 𝜏)) |
38 | 37 | eqcoms 2745 |
. . . . . . . . . . 11
⊢
(⟨⟨𝐴,
𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ → (𝜑 ↔ 𝜏)) |
39 | | opex 5426 |
. . . . . . . . . . . . . 14
⊢
⟨𝑒, 𝑓⟩ ∈ V |
40 | | opex 5426 |
. . . . . . . . . . . . . 14
⊢
⟨𝑔, ℎ⟩ ∈ V |
41 | 39, 40 | opth 5438 |
. . . . . . . . . . . . 13
⊢
(⟨⟨𝑒,
𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ (⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩)) |
42 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑒 ∈ V |
43 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
44 | 42, 43 | opth 5438 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹)) |
45 | | br8.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) |
46 | | br8.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) |
47 | 45, 46 | sylan9bb 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜏 ↔ 𝜁)) |
48 | 44, 47 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ → (𝜏 ↔ 𝜁)) |
49 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ 𝑔 ∈ V |
50 | | vex 3452 |
. . . . . . . . . . . . . . . 16
⊢ ℎ ∈ V |
51 | 49, 50 | opth 5438 |
. . . . . . . . . . . . . . 15
⊢
(⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩ ↔ (𝑔 = 𝐺 ∧ ℎ = 𝐻)) |
52 | | br8.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) |
53 | | br8.8 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) |
54 | 52, 53 | sylan9bb 511 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (𝜁 ↔ 𝜌)) |
55 | 51, 54 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩ → (𝜁 ↔ 𝜌)) |
56 | 48, 55 | sylan9bb 511 |
. . . . . . . . . . . . 13
⊢
((⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝐹⟩ ∧ ⟨𝑔, ℎ⟩ = ⟨𝐺, 𝐻⟩) → (𝜏 ↔ 𝜌)) |
57 | 41, 56 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(⟨⟨𝑒,
𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ → (𝜏 ↔ 𝜌)) |
58 | 57 | eqcoms 2745 |
. . . . . . . . . . 11
⊢
(⟨⟨𝐸,
𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ → (𝜏 ↔ 𝜌)) |
59 | 38, 58 | sylan9bb 511 |
. . . . . . . . . 10
⊢
((⟨⟨𝐴,
𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩) → (𝜑 ↔ 𝜌)) |
60 | 59 | biimp3a 1470 |
. . . . . . . . 9
⊢
((⟨⟨𝐴,
𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌) |
61 | 60 | a1i 11 |
. . . . . . . 8
⊢
((((((((𝑋 ∈
𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) ∧ ℎ ∈ 𝑃) → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
62 | 61 | rexlimdva 3153 |
. . . . . . 7
⊢
(((((((𝑋 ∈
𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
63 | 62 | rexlimdvva 3206 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
64 | 63 | rexlimdvva 3206 |
. . . . 5
⊢
(((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
65 | 64 | rexlimdvva 3206 |
. . . 4
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
66 | 65 | rexlimdvva 3206 |
. . 3
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) → 𝜌)) |
67 | | simpl11 1249 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝑋 ∈ 𝑆) |
68 | | simpl12 1250 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐴 ∈ 𝑄) |
69 | | simpl13 1251 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐵 ∈ 𝑄) |
70 | | simpl21 1252 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐶 ∈ 𝑄) |
71 | | simpl22 1253 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐷 ∈ 𝑄) |
72 | | simpl23 1254 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐸 ∈ 𝑄) |
73 | | simpl31 1255 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐹 ∈ 𝑄) |
74 | | simpl32 1256 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐺 ∈ 𝑄) |
75 | | simpl33 1257 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐻 ∈ 𝑄) |
76 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩) |
77 | | eqidd 2738 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩) |
78 | | simpr 486 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝜌) |
79 | | opeq1 4835 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → ⟨𝑔, ℎ⟩ = ⟨𝐺, ℎ⟩) |
80 | 79 | opeq2d 4842 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩) |
81 | 80 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩)) |
82 | 81, 52 | 3anbi23d 1440 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ∧ 𝜎))) |
83 | | opeq2 4836 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝐻 → ⟨𝐺, ℎ⟩ = ⟨𝐺, 𝐻⟩) |
84 | 83 | opeq2d 4842 |
. . . . . . . . . . 11
⊢ (ℎ = 𝐻 → ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩) |
85 | 84 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (ℎ = 𝐻 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩)) |
86 | 85, 53 | 3anbi23d 1440 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, ℎ⟩⟩ ∧ 𝜎) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜌))) |
87 | 82, 86 | rspc2ev 3595 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄 ∧ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ∧ 𝜌)) → ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁)) |
88 | 74, 75, 76, 77, 78, 87 | syl113anc 1383 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁)) |
89 | | opeq2 4836 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝐷 → ⟨𝐶, 𝑑⟩ = ⟨𝐶, 𝐷⟩) |
90 | 89 | opeq2d 4842 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝐷 → ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩) |
91 | 90 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩)) |
92 | 91, 33 | 3anbi13d 1439 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏))) |
93 | 92 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏))) |
94 | | opeq1 4835 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝐸 → ⟨𝑒, 𝑓⟩ = ⟨𝐸, 𝑓⟩) |
95 | 94 | opeq1d 4841 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩) |
96 | 95 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩)) |
97 | 96, 45 | 3anbi23d 1440 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂))) |
98 | 97 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜏) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂))) |
99 | | opeq2 4836 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → ⟨𝐸, 𝑓⟩ = ⟨𝐸, 𝐹⟩) |
100 | 99 | opeq1d 4841 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩) |
101 | 100 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ↔ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩)) |
102 | 101, 46 | 3anbi23d 1440 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁))) |
103 | 102 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜂) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁))) |
104 | 93, 98, 103 | rspc3ev 3597 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄) ∧ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝐸, 𝐹⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜁)) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)) |
105 | 71, 72, 73, 88, 104 | syl31anc 1374 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)) |
106 | | opeq1 4835 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → ⟨𝑎, 𝑏⟩ = ⟨𝐴, 𝑏⟩) |
107 | 106 | opeq1d 4841 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩) |
108 | 107 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩)) |
109 | 108, 25 | 3anbi13d 1439 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))) |
110 | 109 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))) |
111 | 110 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))) |
112 | 111 | 2rexbidv 3214 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓))) |
113 | | opeq2 4836 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐵 → ⟨𝐴, 𝑏⟩ = ⟨𝐴, 𝐵⟩) |
114 | 113 | opeq1d 4841 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐵 → ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩) |
115 | 114 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩)) |
116 | 115, 26 | 3anbi13d 1439 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒))) |
117 | 116 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒))) |
118 | 117 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒))) |
119 | 118 | 2rexbidv 3214 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒))) |
120 | | opeq1 4835 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐶 → ⟨𝑐, 𝑑⟩ = ⟨𝐶, 𝑑⟩) |
121 | 120 | opeq2d 4842 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐶 → ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩) |
122 | 121 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐶 → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ↔ ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩)) |
123 | 122, 32 | 3anbi13d 1439 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → ((⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃))) |
124 | 123 | rexbidv 3176 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃))) |
125 | 124 | 2rexbidv 3214 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃))) |
126 | 125 | 2rexbidv 3214 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃))) |
127 | 112, 119,
126 | rspc3ev 3597 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜃)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) |
128 | 68, 69, 70, 105, 127 | syl31anc 1374 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) |
129 | | br8.9 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) |
130 | 129 | rexeqdv 3317 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
131 | 129, 130 | rexeqbidv 3323 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
132 | 129, 131 | rexeqbidv 3323 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
133 | 129, 132 | rexeqbidv 3323 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
134 | 129, 133 | rexeqbidv 3323 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
135 | 129, 134 | rexeqbidv 3323 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
136 | 129, 135 | rexeqbidv 3323 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
137 | 129, 136 | rexeqbidv 3323 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
138 | 137 | rspcev 3584 |
. . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) |
139 | 67, 128, 138 | syl2anc 585 |
. . . 4
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑)) |
140 | 139 | ex 414 |
. . 3
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (𝜌 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑))) |
141 | 66, 140 | impbid 211 |
. 2
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩ = ⟨⟨𝑎, 𝑏⟩, ⟨𝑐, 𝑑⟩⟩ ∧ ⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ = ⟨⟨𝑒, 𝑓⟩, ⟨𝑔, ℎ⟩⟩ ∧ 𝜑) ↔ 𝜌)) |
142 | 18, 141 | bitrid 283 |
1
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (⟨⟨𝐴, 𝐵⟩, ⟨𝐶, 𝐷⟩⟩𝑅⟨⟨𝐸, 𝐹⟩, ⟨𝐺, 𝐻⟩⟩ ↔ 𝜌)) |