Step | Hyp | Ref
| Expression |
1 | | df-id 4953 |
. 2
⊢ I =
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} |
2 | | ancom 465 |
. . . . . . . . . . 11
⊢ ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑥 = 𝑧 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
3 | | equcom 1932 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
4 | 3 | anbi1i 727 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑧 ∧ 𝑤 = 〈𝑥, 𝑧〉) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
5 | 2, 4 | bitri 263 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
6 | 5 | exbii 1764 |
. . . . . . . . 9
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
7 | | opeq2 4341 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑥〉) |
8 | 7 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑥〉)) |
9 | 8 | equsexvw 1919 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉) ↔ 𝑤 = 〈𝑥, 𝑥〉) |
10 | | equid 1926 |
. . . . . . . . . 10
⊢ 𝑥 = 𝑥 |
11 | 10 | biantru 525 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑥〉 ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
12 | 6, 9, 11 | 3bitri 285 |
. . . . . . . 8
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
13 | 12 | exbii 1764 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
14 | | nfe1 2014 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) |
15 | 14 | 19.9 2060 |
. . . . . . 7
⊢
(∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
16 | 13, 15 | bitr4i 266 |
. . . . . 6
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
17 | | opeq2 4341 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
18 | 17 | eqeq2d 2620 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑤 = 〈𝑥, 𝑥〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
19 | | equequ2 1940 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 ↔ 𝑥 = 𝑦)) |
20 | 18, 19 | anbi12d 743 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
21 | 20 | sps 2043 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
22 | 21 | drex1 2315 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
23 | 22 | drex2 2316 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
24 | 16, 23 | syl5bb 271 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
25 | | nfnae 2306 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
26 | | nfnae 2306 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
27 | | nfcvd 2752 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
28 | | nfcvf2 2775 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
29 | | nfcvd 2752 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑧) |
30 | 28, 29 | nfopd 4357 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦〈𝑥, 𝑧〉) |
31 | 27, 30 | nfeqd 2758 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = 〈𝑥, 𝑧〉) |
32 | 28, 29 | nfeqd 2758 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧) |
33 | 31, 32 | nfand 1814 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)) |
34 | | opeq2 4341 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑦〉) |
35 | 34 | eqeq2d 2620 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
36 | | equequ2 1940 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
37 | 35, 36 | anbi12d 743 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
38 | 37 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)))) |
39 | 26, 33, 38 | cbvexd 2266 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
40 | 25, 39 | exbid 2078 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
41 | 24, 40 | pm2.61i 175 |
. . . 4
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)) |
42 | 41 | abbii 2726 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
43 | | df-opab 4644 |
. . 3
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} |
44 | | df-opab 4644 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
45 | 42, 43, 44 | 3eqtr4i 2642 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
46 | 1, 45 | eqtri 2632 |
1
⊢ I =
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |