Proof of Theorem br6
Step | Hyp | Ref
| Expression |
1 | | opex 5383 |
. . 3
⊢
〈𝐴, 〈𝐵, 𝐶〉〉 ∈ V |
2 | | opex 5383 |
. . 3
⊢
〈𝐷, 〈𝐸, 𝐹〉〉 ∈ V |
3 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ↔ 〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝑎, 〈𝑏, 𝑐〉〉)) |
4 | | eqcom 2747 |
. . . . . . . . 9
⊢
(〈𝐴,
〈𝐵, 𝐶〉〉 = 〈𝑎, 〈𝑏, 𝑐〉〉 ↔ 〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉) |
5 | 3, 4 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ↔ 〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉)) |
6 | 5 | 3anbi1d 1439 |
. . . . . . 7
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → ((𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑))) |
7 | 6 | rexbidv 3228 |
. . . . . 6
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑))) |
8 | 7 | 2rexbidv 3231 |
. . . . 5
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑))) |
9 | 8 | 2rexbidv 3231 |
. . . 4
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑))) |
10 | 9 | 2rexbidv 3231 |
. . 3
⊢ (𝑝 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑))) |
11 | | eqeq1 2744 |
. . . . . . . . 9
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝑑, 〈𝑒, 𝑓〉〉)) |
12 | | eqcom 2747 |
. . . . . . . . 9
⊢
(〈𝐷,
〈𝐸, 𝐹〉〉 = 〈𝑑, 〈𝑒, 𝑓〉〉 ↔ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉) |
13 | 11, 12 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ↔ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉)) |
14 | 13 | 3anbi2d 1440 |
. . . . . . 7
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → ((〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
15 | 14 | rexbidv 3228 |
. . . . . 6
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
16 | 15 | 2rexbidv 3231 |
. . . . 5
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
17 | 16 | 2rexbidv 3231 |
. . . 4
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
18 | 17 | 2rexbidv 3231 |
. . 3
⊢ (𝑞 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑) ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
19 | | br6.8 |
. . 3
⊢ 𝑅 = {〈𝑝, 𝑞〉 ∣ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (𝑝 = 〈𝑎, 〈𝑏, 𝑐〉〉 ∧ 𝑞 = 〈𝑑, 〈𝑒, 𝑓〉〉 ∧ 𝜑)} |
20 | 1, 2, 10, 18, 19 | brab 5459 |
. 2
⊢
(〈𝐴,
〈𝐵, 𝐶〉〉𝑅〈𝐷, 〈𝐸, 𝐹〉〉 ↔ ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) |
21 | | vex 3435 |
. . . . . . . . . . . 12
⊢ 𝑎 ∈ V |
22 | | opex 5383 |
. . . . . . . . . . . 12
⊢
〈𝑏, 𝑐〉 ∈ V |
23 | 21, 22 | opth 5395 |
. . . . . . . . . . 11
⊢
(〈𝑎,
〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ↔ (𝑎 = 𝐴 ∧ 〈𝑏, 𝑐〉 = 〈𝐵, 𝐶〉)) |
24 | | br6.1 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝐴 → (𝜑 ↔ 𝜓)) |
25 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑏 ∈ V |
26 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑐 ∈ V |
27 | 25, 26 | opth 5395 |
. . . . . . . . . . . . 13
⊢
(〈𝑏, 𝑐〉 = 〈𝐵, 𝐶〉 ↔ (𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) |
28 | | br6.2 |
. . . . . . . . . . . . . 14
⊢ (𝑏 = 𝐵 → (𝜓 ↔ 𝜒)) |
29 | | br6.3 |
. . . . . . . . . . . . . 14
⊢ (𝑐 = 𝐶 → (𝜒 ↔ 𝜃)) |
30 | 28, 29 | sylan9bb 510 |
. . . . . . . . . . . . 13
⊢ ((𝑏 = 𝐵 ∧ 𝑐 = 𝐶) → (𝜓 ↔ 𝜃)) |
31 | 27, 30 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(〈𝑏, 𝑐〉 = 〈𝐵, 𝐶〉 → (𝜓 ↔ 𝜃)) |
32 | 24, 31 | sylan9bb 510 |
. . . . . . . . . . 11
⊢ ((𝑎 = 𝐴 ∧ 〈𝑏, 𝑐〉 = 〈𝐵, 𝐶〉) → (𝜑 ↔ 𝜃)) |
33 | 23, 32 | sylbi 216 |
. . . . . . . . . 10
⊢
(〈𝑎,
〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 → (𝜑 ↔ 𝜃)) |
34 | | vex 3435 |
. . . . . . . . . . . 12
⊢ 𝑑 ∈ V |
35 | | opex 5383 |
. . . . . . . . . . . 12
⊢
〈𝑒, 𝑓〉 ∈ V |
36 | 34, 35 | opth 5395 |
. . . . . . . . . . 11
⊢
(〈𝑑,
〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ↔ (𝑑 = 𝐷 ∧ 〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉)) |
37 | | br6.4 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝐷 → (𝜃 ↔ 𝜏)) |
38 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑒 ∈ V |
39 | | vex 3435 |
. . . . . . . . . . . . . 14
⊢ 𝑓 ∈ V |
40 | 38, 39 | opth 5395 |
. . . . . . . . . . . . 13
⊢
(〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 ↔ (𝑒 = 𝐸 ∧ 𝑓 = 𝐹)) |
41 | | br6.5 |
. . . . . . . . . . . . . 14
⊢ (𝑒 = 𝐸 → (𝜏 ↔ 𝜂)) |
42 | | br6.6 |
. . . . . . . . . . . . . 14
⊢ (𝑓 = 𝐹 → (𝜂 ↔ 𝜁)) |
43 | 41, 42 | sylan9bb 510 |
. . . . . . . . . . . . 13
⊢ ((𝑒 = 𝐸 ∧ 𝑓 = 𝐹) → (𝜏 ↔ 𝜁)) |
44 | 40, 43 | sylbi 216 |
. . . . . . . . . . . 12
⊢
(〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉 → (𝜏 ↔ 𝜁)) |
45 | 37, 44 | sylan9bb 510 |
. . . . . . . . . . 11
⊢ ((𝑑 = 𝐷 ∧ 〈𝑒, 𝑓〉 = 〈𝐸, 𝐹〉) → (𝜃 ↔ 𝜁)) |
46 | 36, 45 | sylbi 216 |
. . . . . . . . . 10
⊢
(〈𝑑,
〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 → (𝜃 ↔ 𝜁)) |
47 | 33, 46 | sylan9bb 510 |
. . . . . . . . 9
⊢
((〈𝑎,
〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉) → (𝜑 ↔ 𝜁)) |
48 | 47 | biimp3a 1468 |
. . . . . . . 8
⊢
((〈𝑎,
〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁) |
49 | 48 | a1i 11 |
. . . . . . 7
⊢
((((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) ∧ 𝑓 ∈ 𝑃) → ((〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁)) |
50 | 49 | rexlimdva 3215 |
. . . . . 6
⊢
(((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) ∧ (𝑑 ∈ 𝑃 ∧ 𝑒 ∈ 𝑃)) → (∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁)) |
51 | 50 | rexlimdvva 3225 |
. . . . 5
⊢ ((((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) ∧ (𝑏 ∈ 𝑃 ∧ 𝑐 ∈ 𝑃)) → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁)) |
52 | 51 | rexlimdvva 3225 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ (𝑥 ∈ 𝑆 ∧ 𝑎 ∈ 𝑃)) → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁)) |
53 | 52 | rexlimdvva 3225 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) → 𝜁)) |
54 | | simpl1 1190 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → 𝑋 ∈ 𝑆) |
55 | | simpl2 1191 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄)) |
56 | | opeq1 4810 |
. . . . . . . . . 10
⊢ (𝑑 = 𝐷 → 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝑒, 𝑓〉〉) |
57 | 56 | eqeq1d 2742 |
. . . . . . . . 9
⊢ (𝑑 = 𝐷 → (〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉)) |
58 | 57, 37 | 3anbi23d 1438 |
. . . . . . . 8
⊢ (𝑑 = 𝐷 → ((〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃) ↔ (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜏))) |
59 | | opeq1 4810 |
. . . . . . . . . . 11
⊢ (𝑒 = 𝐸 → 〈𝑒, 𝑓〉 = 〈𝐸, 𝑓〉) |
60 | 59 | opeq2d 4817 |
. . . . . . . . . 10
⊢ (𝑒 = 𝐸 → 〈𝐷, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝑓〉〉) |
61 | 60 | eqeq1d 2742 |
. . . . . . . . 9
⊢ (𝑒 = 𝐸 → (〈𝐷, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉)) |
62 | 61, 41 | 3anbi23d 1438 |
. . . . . . . 8
⊢ (𝑒 = 𝐸 → ((〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜏) ↔ (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜂))) |
63 | | opeq2 4811 |
. . . . . . . . . . . 12
⊢ (𝑓 = 𝐹 → 〈𝐸, 𝑓〉 = 〈𝐸, 𝐹〉) |
64 | 63 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (𝑓 = 𝐹 → 〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉) |
65 | 64 | eqeq1d 2742 |
. . . . . . . . . 10
⊢ (𝑓 = 𝐹 → (〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉)) |
66 | 65, 42 | 3anbi23d 1438 |
. . . . . . . . 9
⊢ (𝑓 = 𝐹 → ((〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜂) ↔ (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜁))) |
67 | | eqid 2740 |
. . . . . . . . . . 11
⊢
〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 |
68 | | eqid 2740 |
. . . . . . . . . . 11
⊢
〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 |
69 | 67, 68 | pm3.2i 471 |
. . . . . . . . . 10
⊢
(〈𝐴,
〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉) |
70 | | df-3an 1088 |
. . . . . . . . . 10
⊢
((〈𝐴,
〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜁) ↔ ((〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉) ∧ 𝜁)) |
71 | 69, 70 | mpbiran 706 |
. . . . . . . . 9
⊢
((〈𝐴,
〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝐹〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜁) ↔ 𝜁) |
72 | 66, 71 | bitrdi 287 |
. . . . . . . 8
⊢ (𝑓 = 𝐹 → ((〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝐷, 〈𝐸, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜂) ↔ 𝜁)) |
73 | 58, 62, 72 | rspc3ev 3575 |
. . . . . . 7
⊢ (((𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃)) |
74 | 73 | 3ad2antl3 1186 |
. . . . . 6
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃)) |
75 | | opeq1 4810 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝐴 → 〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝑏, 𝑐〉〉) |
76 | 75 | eqeq1d 2742 |
. . . . . . . . . 10
⊢ (𝑎 = 𝐴 → (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ↔ 〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉)) |
77 | 76, 24 | 3anbi13d 1437 |
. . . . . . . . 9
⊢ (𝑎 = 𝐴 → ((〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓))) |
78 | 77 | rexbidv 3228 |
. . . . . . . 8
⊢ (𝑎 = 𝐴 → (∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓))) |
79 | 78 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑎 = 𝐴 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓))) |
80 | | opeq1 4810 |
. . . . . . . . . . . 12
⊢ (𝑏 = 𝐵 → 〈𝑏, 𝑐〉 = 〈𝐵, 𝑐〉) |
81 | 80 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → 〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝑐〉〉) |
82 | 81 | eqeq1d 2742 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ↔ 〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉)) |
83 | 82, 28 | 3anbi13d 1437 |
. . . . . . . . 9
⊢ (𝑏 = 𝐵 → ((〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓) ↔ (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒))) |
84 | 83 | rexbidv 3228 |
. . . . . . . 8
⊢ (𝑏 = 𝐵 → (∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓) ↔ ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒))) |
85 | 84 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑏 = 𝐵 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜓) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒))) |
86 | | opeq2 4811 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝐶 → 〈𝐵, 𝑐〉 = 〈𝐵, 𝐶〉) |
87 | 86 | opeq2d 4817 |
. . . . . . . . . . 11
⊢ (𝑐 = 𝐶 → 〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉) |
88 | 87 | eqeq1d 2742 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ↔ 〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉)) |
89 | 88, 29 | 3anbi13d 1437 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → ((〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒) ↔ (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃))) |
90 | 89 | rexbidv 3228 |
. . . . . . . 8
⊢ (𝑐 = 𝐶 → (∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒) ↔ ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃))) |
91 | 90 | 2rexbidv 3231 |
. . . . . . 7
⊢ (𝑐 = 𝐶 → (∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜒) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃))) |
92 | 79, 85, 91 | rspc3ev 3575 |
. . . . . 6
⊢ (((𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝐴, 〈𝐵, 𝐶〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜃)) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) |
93 | 55, 74, 92 | syl2anc 584 |
. . . . 5
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) |
94 | | br6.7 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → 𝑃 = 𝑄) |
95 | 94 | rexeqdv 3348 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑋 → (∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
96 | 94, 95 | rexeqbidv 3336 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑋 → (∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
97 | 94, 96 | rexeqbidv 3336 |
. . . . . . . . 9
⊢ (𝑥 = 𝑋 → (∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
98 | 94, 97 | rexeqbidv 3336 |
. . . . . . . 8
⊢ (𝑥 = 𝑋 → (∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
99 | 94, 98 | rexeqbidv 3336 |
. . . . . . 7
⊢ (𝑥 = 𝑋 → (∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
100 | 94, 99 | rexeqbidv 3336 |
. . . . . 6
⊢ (𝑥 = 𝑋 → (∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
101 | 100 | rspcev 3561 |
. . . . 5
⊢ ((𝑋 ∈ 𝑆 ∧ ∃𝑎 ∈ 𝑄 ∃𝑏 ∈ 𝑄 ∃𝑐 ∈ 𝑄 ∃𝑑 ∈ 𝑄 ∃𝑒 ∈ 𝑄 ∃𝑓 ∈ 𝑄 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) |
102 | 54, 93, 101 | syl2anc 584 |
. . . 4
⊢ (((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) ∧ 𝜁) → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑)) |
103 | 102 | ex 413 |
. . 3
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (𝜁 → ∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑))) |
104 | 53, 103 | impbid 211 |
. 2
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (∃𝑥 ∈ 𝑆 ∃𝑎 ∈ 𝑃 ∃𝑏 ∈ 𝑃 ∃𝑐 ∈ 𝑃 ∃𝑑 ∈ 𝑃 ∃𝑒 ∈ 𝑃 ∃𝑓 ∈ 𝑃 (〈𝑎, 〈𝑏, 𝑐〉〉 = 〈𝐴, 〈𝐵, 𝐶〉〉 ∧ 〈𝑑, 〈𝑒, 𝑓〉〉 = 〈𝐷, 〈𝐸, 𝐹〉〉 ∧ 𝜑) ↔ 𝜁)) |
105 | 20, 104 | syl5bb 283 |
1
⊢ ((𝑋 ∈ 𝑆 ∧ (𝐴 ∈ 𝑄 ∧ 𝐵 ∈ 𝑄 ∧ 𝐶 ∈ 𝑄) ∧ (𝐷 ∈ 𝑄 ∧ 𝐸 ∈ 𝑄 ∧ 𝐹 ∈ 𝑄)) → (〈𝐴, 〈𝐵, 𝐶〉〉𝑅〈𝐷, 〈𝐸, 𝐹〉〉 ↔ 𝜁)) |