Proof of Theorem br8
Step | Hyp | Ref
| Expression |
1 | | opex 5382 |
. . 3
⊢
〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∈ V |
2 | | opex 5382 |
. . 3
⊢
〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ∈ V |
3 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ↔ 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉)) |
4 | 3 | 3anbi1d 1439 |
. . . . . . . 8
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → ((𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
5 | 4 | rexbidv 3228 |
. . . . . . 7
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
6 | 5 | 2rexbidv 3231 |
. . . . . 6
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
7 | 6 | 2rexbidv 3231 |
. . . . 5
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
8 | 7 | 2rexbidv 3231 |
. . . 4
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
9 | 8 | 2rexbidv 3231 |
. . 3
⊢ (𝑝 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
10 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉)) |
11 | 10 | 3anbi2d 1440 |
. . . . . . . 8
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
12 | 11 | rexbidv 3228 |
. . . . . . 7
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
13 | 12 | 2rexbidv 3231 |
. . . . . 6
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
14 | 13 | 2rexbidv 3231 |
. . . . 5
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
15 | 14 | 2rexbidv 3231 |
. . . 4
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
16 | 15 | 2rexbidv 3231 |
. . 3
⊢ (𝑞 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
17 | | br8.10 |
. . 3
⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (𝑝 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 𝑞 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)} |
18 | 1, 2, 9, 16, 17 | brab 5458 |
. 2
⊢
(〈〈𝐴,
𝐵〉, 〈𝐶, 𝐷〉〉𝑅〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) |
19 | | opex 5382 |
. . . . . . . . . . . . . 14
⊢
〈𝑎, 𝑏〉 ∈ V |
20 | | opex 5382 |
. . . . . . . . . . . . . 14
⊢
〈𝑐, 𝑑〉 ∈ V |
21 | 19, 20 | opth 5394 |
. . . . . . . . . . . . 13
⊢
(〈〈𝑎,
𝑏〉, 〈𝑐, 𝑑〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ↔ (〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉)) |
22 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑎 ∈ V |
23 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑏 ∈ V |
24 | 22, 23 | opth 5394 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵)) |
25 | | br8.1 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) |
26 | | br8.2 |
. . . . . . . . . . . . . . . 16
⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) |
27 | 25, 26 | sylan9bb 510 |
. . . . . . . . . . . . . . 15
⊢ ((𝑎 = 𝐴 ∧ 𝑏 = 𝐵) → (𝜑 ↔ 𝜒)) |
28 | 24, 27 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 → (𝜑 ↔ 𝜒)) |
29 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑐 ∈ V |
30 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑑 ∈ V |
31 | 29, 30 | opth 5394 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 ↔ (𝑐 = 𝐶 ∧ 𝑑 = 𝐷)) |
32 | | br8.3 |
. . . . . . . . . . . . . . . 16
⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) |
33 | | br8.4 |
. . . . . . . . . . . . . . . 16
⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) |
34 | 32, 33 | sylan9bb 510 |
. . . . . . . . . . . . . . 15
⊢ ((𝑐 = 𝐶 ∧ 𝑑 = 𝐷) → (𝜒 ↔ 𝜏)) |
35 | 31, 34 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉 → (𝜒 ↔ 𝜏)) |
36 | 28, 35 | sylan9bb 510 |
. . . . . . . . . . . . 13
⊢
((〈𝑎, 𝑏〉 = 〈𝐴, 𝐵〉 ∧ 〈𝑐, 𝑑〉 = 〈𝐶, 𝐷〉) → (𝜑 ↔ 𝜏)) |
37 | 21, 36 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(〈〈𝑎,
𝑏〉, 〈𝑐, 𝑑〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 → (𝜑 ↔ 𝜏)) |
38 | 37 | eqcoms 2748 |
. . . . . . . . . . 11
⊢
(〈〈𝐴,
𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 → (𝜑 ↔ 𝜏)) |
39 | | opex 5382 |
. . . . . . . . . . . . . 14
⊢
〈𝑒, 𝑓〉 ∈ V |
40 | | opex 5382 |
. . . . . . . . . . . . . 14
⊢
〈𝑔, ℎ〉 ∈ V |
41 | 39, 40 | opth 5394 |
. . . . . . . . . . . . 13
⊢
(〈〈𝑒,
𝑓〉, 〈𝑔, ℎ〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ (〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 ∧ 〈𝑔, ℎ〉 = 〈𝐺, 𝐻〉)) |
42 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑒 ∈ V |
43 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑓 ∈ V |
44 | 42, 43 | opth 5394 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹)) |
45 | | br8.5 |
. . . . . . . . . . . . . . . 16
⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) |
46 | | br8.6 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) |
47 | 45, 46 | sylan9bb 510 |
. . . . . . . . . . . . . . 15
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜏 ↔ 𝜁)) |
48 | 44, 47 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 → (𝜏 ↔ 𝜁)) |
49 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ 𝑔 ∈ V |
50 | | vex 3435 |
. . . . . . . . . . . . . . . 16
⊢ ℎ ∈ V |
51 | 49, 50 | opth 5394 |
. . . . . . . . . . . . . . 15
⊢
(〈𝑔, ℎ〉 = 〈𝐺, 𝐻〉 ↔ (𝑔 = 𝐺 ∧ ℎ = 𝐻)) |
52 | | br8.7 |
. . . . . . . . . . . . . . . 16
⊢ (𝑔 = 𝐺 → (𝜁 ↔ 𝜎)) |
53 | | br8.8 |
. . . . . . . . . . . . . . . 16
⊢ (ℎ = 𝐻 → (𝜎 ↔ 𝜌)) |
54 | 52, 53 | sylan9bb 510 |
. . . . . . . . . . . . . . 15
⊢ ((𝑔 = 𝐺 ∧ ℎ = 𝐻) → (𝜁 ↔ 𝜌)) |
55 | 51, 54 | sylbi 216 |
. . . . . . . . . . . . . 14
⊢
(〈𝑔, ℎ〉 = 〈𝐺, 𝐻〉 → (𝜁 ↔ 𝜌)) |
56 | 48, 55 | sylan9bb 510 |
. . . . . . . . . . . . 13
⊢
((〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 ∧ 〈𝑔, ℎ〉 = 〈𝐺, 𝐻〉) → (𝜏 ↔ 𝜌)) |
57 | 41, 56 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(〈〈𝑒,
𝑓〉, 〈𝑔, ℎ〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 → (𝜏 ↔ 𝜌)) |
58 | 57 | eqcoms 2748 |
. . . . . . . . . . 11
⊢
(〈〈𝐸,
𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 → (𝜏 ↔ 𝜌)) |
59 | 38, 58 | sylan9bb 510 |
. . . . . . . . . 10
⊢
((〈〈𝐴,
𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉) → (𝜑 ↔ 𝜌)) |
60 | 59 | biimp3a 1468 |
. . . . . . . . 9
⊢
((〈〈𝐴,
𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌) |
61 | 60 | a1i 11 |
. . . . . . . 8
⊢
((((((((𝑋 ∈
𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) ∧ ℎ ∈ 𝑃) → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
62 | 61 | rexlimdva 3215 |
. . . . . . 7
⊢
(((((((𝑋 ∈
𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ (𝑓 ∈ 𝑃 ∧ 𝑔 ∈ 𝑃)) → (∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
63 | 62 | rexlimdvva 3225 |
. . . . . 6
⊢
((((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
64 | 63 | rexlimdvva 3225 |
. . . . 5
⊢
(((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
65 | 64 | rexlimdvva 3225 |
. . . 4
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
66 | 65 | rexlimdvva 3225 |
. . 3
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) → 𝜌)) |
67 | | simpl11 1247 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝑋 ∈ 𝑆) |
68 | | simpl12 1248 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐴 ∈ 𝑄) |
69 | | simpl13 1249 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐵 ∈ 𝑄) |
70 | | simpl21 1250 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐶 ∈ 𝑄) |
71 | | simpl22 1251 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐷 ∈ 𝑄) |
72 | | simpl23 1252 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐸 ∈ 𝑄) |
73 | | simpl31 1253 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐹 ∈ 𝑄) |
74 | | simpl32 1254 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐺 ∈ 𝑄) |
75 | | simpl33 1255 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝐻 ∈ 𝑄) |
76 | | eqidd 2741 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉) |
77 | | eqidd 2741 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉) |
78 | | simpr 485 |
. . . . . . . 8
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → 𝜌) |
79 | | opeq1 4810 |
. . . . . . . . . . . 12
⊢ (𝑔 = 𝐺 → 〈𝑔, ℎ〉 = 〈𝐺, ℎ〉) |
80 | 79 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (𝑔 = 𝐺 → 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉) |
81 | 80 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑔 = 𝐺 → (〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉)) |
82 | 81, 52 | 3anbi23d 1438 |
. . . . . . . . 9
⊢ (𝑔 = 𝐺 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉 ∧ 𝜎))) |
83 | | opeq2 4811 |
. . . . . . . . . . . 12
⊢ (ℎ = 𝐻 → 〈𝐺, ℎ〉 = 〈𝐺, 𝐻〉) |
84 | 83 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (ℎ = 𝐻 → 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉) |
85 | 84 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (ℎ = 𝐻 → (〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉)) |
86 | 85, 53 | 3anbi23d 1438 |
. . . . . . . . 9
⊢ (ℎ = 𝐻 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, ℎ〉〉 ∧ 𝜎) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ∧ 𝜌))) |
87 | 82, 86 | rspc2ev 3573 |
. . . . . . . 8
⊢ ((𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄 ∧ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ∧ 𝜌)) → ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁)) |
88 | 74, 75, 76, 77, 78, 87 | syl113anc 1381 |
. . . . . . 7
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁)) |
89 | | opeq2 4811 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝐷 → 〈𝐶, 𝑑〉 = 〈𝐶, 𝐷〉) |
90 | 89 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝐷 → 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉) |
91 | 90 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ↔ 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉)) |
92 | 91, 33 | 3anbi13d 1437 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜏))) |
93 | 92 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜏))) |
94 | | opeq1 4810 |
. . . . . . . . . . . 12
⊢ (𝑒 = 𝐸 → 〈𝑒, 𝑓〉 = 〈𝐸, 𝑓〉) |
95 | 94 | opeq1d 4816 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉) |
96 | 95 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → (〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉)) |
97 | 96, 45 | 3anbi23d 1438 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜏) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜂))) |
98 | 97 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜏) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜂))) |
99 | | opeq2 4811 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → 〈𝐸, 𝑓〉 = 〈𝐸, 𝐹〉) |
100 | 99 | opeq1d 4816 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉) |
101 | 100 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 ↔ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉)) |
102 | 101, 46 | 3anbi23d 1438 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜂) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁))) |
103 | 102 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → (∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜂) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁))) |
104 | 93, 98, 103 | rspc3ev 3575 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄) ∧ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝐸, 𝐹〉, 〈𝑔, ℎ〉〉 ∧ 𝜁)) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃)) |
105 | 71, 72, 73, 88, 104 | syl31anc 1372 |
. . . . . 6
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃)) |
106 | | opeq1 4810 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝐴 → 〈𝑎, 𝑏〉 = 〈𝐴, 𝑏〉) |
107 | 106 | opeq1d 4816 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉) |
108 | 107 | eqeq2d 2751 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ↔ 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉)) |
109 | 108, 25 | 3anbi13d 1437 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓))) |
110 | 109 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → (∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓))) |
111 | 110 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓))) |
112 | 111 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓))) |
113 | | opeq2 4811 |
. . . . . . . . . . . . 13
⊢ (𝑏 = 𝐵 → 〈𝐴, 𝑏〉 = 〈𝐴, 𝐵〉) |
114 | 113 | opeq1d 4816 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐵 → 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉) |
115 | 114 | eqeq2d 2751 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ↔ 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉)) |
116 | 115, 26 | 3anbi13d 1437 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒))) |
117 | 116 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → (∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓) ↔ ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒))) |
118 | 117 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒))) |
119 | 118 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒))) |
120 | | opeq1 4810 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝐶 → 〈𝑐, 𝑑〉 = 〈𝐶, 𝑑〉) |
121 | 120 | opeq2d 4817 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐶 → 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉) |
122 | 121 | eqeq2d 2751 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐶 → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ↔ 〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉)) |
123 | 122, 32 | 3anbi13d 1437 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → ((〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒) ↔ (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃))) |
124 | 123 | rexbidv 3228 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒) ↔ ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃))) |
125 | 124 | 2rexbidv 3231 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃))) |
126 | 125 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃))) |
127 | 112, 119,
126 | rspc3ev 3575 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝐴, 𝐵〉, 〈𝐶, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜃)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) |
128 | 68, 69, 70, 105, 127 | syl31anc 1372 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) |
129 | | br8.9 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) |
130 | 129 | rexeqdv 3348 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑋 → (∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
131 | 129, 130 | rexeqbidv 3336 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑋 → (∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
132 | 129, 131 | rexeqbidv 3336 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
133 | 129, 132 | rexeqbidv 3336 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
134 | 129, 133 | rexeqbidv 3336 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
135 | 129, 134 | rexeqbidv 3336 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
136 | 129, 135 | rexeqbidv 3336 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
137 | 129, 136 | rexeqbidv 3336 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
138 | 137 | rspcev 3561 |
. . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 ∃𝑔 ∈ 𝑄 ∃ℎ ∈ 𝑄 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) |
139 | 67, 128, 138 | syl2anc 584 |
. . . 4
⊢ ((((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) ∧ 𝜌) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑)) |
140 | 139 | ex 413 |
. . 3
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (𝜌 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑))) |
141 | 66, 140 | impbid 211 |
. 2
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 ∃𝑔 ∈ 𝑃 ∃ℎ ∈ 𝑃 (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉 = 〈〈𝑎, 𝑏〉, 〈𝑐, 𝑑〉〉 ∧ 〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 = 〈〈𝑒, 𝑓〉, 〈𝑔, ℎ〉〉 ∧ 𝜑) ↔ 𝜌)) |
142 | 18, 141 | syl5bb 283 |
1
⊢ (((𝑋 ∈ 𝑆 ∧ 𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄) ∧ (𝐶 ∈ 𝑄 ∧ 𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄) ∧ (𝐹 ∈ 𝑄 ∧ 𝐺 ∈ 𝑄 ∧ 𝐻 ∈ 𝑄)) → (〈〈𝐴, 𝐵〉, 〈𝐶, 𝐷〉〉𝑅〈〈𝐸, 𝐹〉, 〈𝐺, 𝐻〉〉 ↔ 𝜌)) |