Step | Hyp | Ref
| Expression |
1 | | euotd.4 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝜓 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶))) |
2 | 1 | biimpa 477 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝜓) → (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) |
3 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑎 ∈ V |
4 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑏 ∈ V |
5 | | vex 3435 |
. . . . . . . . . . . . 13
⊢ 𝑐 ∈ V |
6 | 3, 4, 5 | otth 5402 |
. . . . . . . . . . . 12
⊢
(〈𝑎, 𝑏, 𝑐〉 = 〈𝐴, 𝐵, 𝐶〉 ↔ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) |
7 | 2, 6 | sylibr 233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝜓) → 〈𝑎, 𝑏, 𝑐〉 = 〈𝐴, 𝐵, 𝐶〉) |
8 | 7 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝜓) → (𝑥 = 〈𝑎, 𝑏, 𝑐〉 ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
9 | 8 | biimpd 228 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝜓) → (𝑥 = 〈𝑎, 𝑏, 𝑐〉 → 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
10 | 9 | impancom 452 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 = 〈𝑎, 𝑏, 𝑐〉) → (𝜓 → 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
11 | 10 | expimpd 454 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) → 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
12 | 11 | exlimdv 1940 |
. . . . . 6
⊢ (𝜑 → (∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) → 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
13 | 12 | exlimdvv 1941 |
. . . . 5
⊢ (𝜑 → (∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) → 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
14 | | euotd.3 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ 𝑊) |
15 | | euotd.2 |
. . . . . . . . 9
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
16 | | tru 1546 |
. . . . . . . . . . 11
⊢
⊤ |
17 | | euotd.1 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
18 | 15 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → 𝐵 ∈ 𝑉) |
19 | 14 | ad2antrr 723 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → 𝐶 ∈ 𝑊) |
20 | | simpr 485 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) |
21 | 20, 6 | sylibr 233 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → 〈𝑎, 𝑏, 𝑐〉 = 〈𝐴, 𝐵, 𝐶〉) |
22 | 21 | eqcomd 2746 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → 〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉) |
23 | 1 | biimpar 478 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → 𝜓) |
24 | 22, 23 | jca 512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → (〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
25 | | trud 1552 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ⊤) |
26 | 24, 25 | 2thd 264 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑎 = 𝐴 ∧ 𝑏 = 𝐵 ∧ 𝑐 = 𝐶)) → ((〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ⊤)) |
27 | 26 | 3anassrs 1359 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) ∧ 𝑐 = 𝐶) → ((〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ⊤)) |
28 | 19, 27 | sbcied 3765 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑎 = 𝐴) ∧ 𝑏 = 𝐵) → ([𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ⊤)) |
29 | 18, 28 | sbcied 3765 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑎 = 𝐴) → ([𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ⊤)) |
30 | 17, 29 | sbcied 3765 |
. . . . . . . . . . 11
⊢ (𝜑 → ([𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ⊤)) |
31 | 16, 30 | mpbiri 257 |
. . . . . . . . . 10
⊢ (𝜑 → [𝐴 / 𝑎][𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
32 | 31 | spesbcd 3821 |
. . . . . . . . 9
⊢ (𝜑 → ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
33 | | nfcv 2909 |
. . . . . . . . . 10
⊢
Ⅎ𝑏𝐵 |
34 | | nfsbc1v 3740 |
. . . . . . . . . . 11
⊢
Ⅎ𝑏[𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) |
35 | 34 | nfex 2322 |
. . . . . . . . . 10
⊢
Ⅎ𝑏∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) |
36 | | sbceq1a 3731 |
. . . . . . . . . . 11
⊢ (𝑏 = 𝐵 → ([𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ [𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
37 | 36 | exbidv 1928 |
. . . . . . . . . 10
⊢ (𝑏 = 𝐵 → (∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
38 | 33, 35, 37 | spcegf 3530 |
. . . . . . . . 9
⊢ (𝐵 ∈ 𝑉 → (∃𝑎[𝐵 / 𝑏][𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) → ∃𝑏∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
39 | 15, 32, 38 | sylc 65 |
. . . . . . . 8
⊢ (𝜑 → ∃𝑏∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
40 | | nfcv 2909 |
. . . . . . . . 9
⊢
Ⅎ𝑐𝐶 |
41 | | nfsbc1v 3740 |
. . . . . . . . . . 11
⊢
Ⅎ𝑐[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) |
42 | 41 | nfex 2322 |
. . . . . . . . . 10
⊢
Ⅎ𝑐∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) |
43 | 42 | nfex 2322 |
. . . . . . . . 9
⊢
Ⅎ𝑐∃𝑏∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) |
44 | | sbceq1a 3731 |
. . . . . . . . . 10
⊢ (𝑐 = 𝐶 → ((〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ [𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
45 | 44 | 2exbidv 1931 |
. . . . . . . . 9
⊢ (𝑐 = 𝐶 → (∃𝑏∃𝑎(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ∃𝑏∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
46 | 40, 43, 45 | spcegf 3530 |
. . . . . . . 8
⊢ (𝐶 ∈ 𝑊 → (∃𝑏∃𝑎[𝐶 / 𝑐](〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) → ∃𝑐∃𝑏∃𝑎(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
47 | 14, 39, 46 | sylc 65 |
. . . . . . 7
⊢ (𝜑 → ∃𝑐∃𝑏∃𝑎(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
48 | | excom13 2168 |
. . . . . . 7
⊢
(∃𝑐∃𝑏∃𝑎(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ∃𝑎∃𝑏∃𝑐(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
49 | 47, 48 | sylib 217 |
. . . . . 6
⊢ (𝜑 → ∃𝑎∃𝑏∃𝑐(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |
50 | | eqeq1 2744 |
. . . . . . . 8
⊢ (𝑥 = 〈𝐴, 𝐵, 𝐶〉 → (𝑥 = 〈𝑎, 𝑏, 𝑐〉 ↔ 〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉)) |
51 | 50 | anbi1d 630 |
. . . . . . 7
⊢ (𝑥 = 〈𝐴, 𝐵, 𝐶〉 → ((𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ (〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
52 | 51 | 3exbidv 1932 |
. . . . . 6
⊢ (𝑥 = 〈𝐴, 𝐵, 𝐶〉 → (∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ∃𝑎∃𝑏∃𝑐(〈𝐴, 𝐵, 𝐶〉 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
53 | 49, 52 | syl5ibrcom 246 |
. . . . 5
⊢ (𝜑 → (𝑥 = 〈𝐴, 𝐵, 𝐶〉 → ∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓))) |
54 | 13, 53 | impbid 211 |
. . . 4
⊢ (𝜑 → (∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
55 | 54 | alrimiv 1934 |
. . 3
⊢ (𝜑 → ∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
56 | | otex 5383 |
. . . 4
⊢
〈𝐴, 𝐵, 𝐶〉 ∈ V |
57 | | eqeq2 2752 |
. . . . . 6
⊢ (𝑦 = 〈𝐴, 𝐵, 𝐶〉 → (𝑥 = 𝑦 ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉)) |
58 | 57 | bibi2d 343 |
. . . . 5
⊢ (𝑦 = 〈𝐴, 𝐵, 𝐶〉 → ((∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ (∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉))) |
59 | 58 | albidv 1927 |
. . . 4
⊢ (𝑦 = 〈𝐴, 𝐵, 𝐶〉 → (∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 𝑦) ↔ ∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉))) |
60 | 56, 59 | spcev 3544 |
. . 3
⊢
(∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 〈𝐴, 𝐵, 𝐶〉) → ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 𝑦)) |
61 | 55, 60 | syl 17 |
. 2
⊢ (𝜑 → ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 𝑦)) |
62 | | eu6 2576 |
. 2
⊢
(∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ ∃𝑦∀𝑥(∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓) ↔ 𝑥 = 𝑦)) |
63 | 61, 62 | sylibr 233 |
1
⊢ (𝜑 → ∃!𝑥∃𝑎∃𝑏∃𝑐(𝑥 = 〈𝑎, 𝑏, 𝑐〉 ∧ 𝜓)) |