Step | Hyp | Ref
| Expression |
1 | | df-id 5455 |
. 2
⊢ I =
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} |
2 | | equcom 2026 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
3 | 2 | anbi1ci 629 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
4 | 3 | exbii 1855 |
. . . . . . . . 9
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
5 | | opeq2 4785 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑥〉) |
6 | 5 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑥〉)) |
7 | 6 | equsexvw 2013 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉) ↔ 𝑤 = 〈𝑥, 𝑥〉) |
8 | | equid 2020 |
. . . . . . . . . 10
⊢ 𝑥 = 𝑥 |
9 | 8 | biantru 533 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑥〉 ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
10 | 4, 7, 9 | 3bitri 300 |
. . . . . . . 8
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
11 | 10 | exbii 1855 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
12 | | nfe1 2151 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) |
13 | 12 | 19.9 2203 |
. . . . . . 7
⊢
(∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
14 | 11, 13 | bitr4i 281 |
. . . . . 6
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
15 | | opeq2 4785 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
16 | 15 | eqeq2d 2748 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑤 = 〈𝑥, 𝑥〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
17 | | equequ2 2034 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 ↔ 𝑥 = 𝑦)) |
18 | 16, 17 | anbi12d 634 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
19 | 18 | sps 2182 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
20 | 19 | drex1 2440 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
21 | 20 | drex2 2441 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
22 | 14, 21 | syl5bb 286 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
23 | | nfnae 2433 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
24 | | nfnae 2433 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
25 | | nfcvd 2905 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
26 | | nfcvf2 2934 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
27 | | nfcvd 2905 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑧) |
28 | 26, 27 | nfopd 4801 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦〈𝑥, 𝑧〉) |
29 | 25, 28 | nfeqd 2914 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = 〈𝑥, 𝑧〉) |
30 | 26, 27 | nfeqd 2914 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧) |
31 | 29, 30 | nfand 1905 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)) |
32 | | opeq2 4785 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑦〉) |
33 | 32 | eqeq2d 2748 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
34 | | equequ2 2034 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
35 | 33, 34 | anbi12d 634 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)))) |
37 | 24, 31, 36 | cbvexd 2407 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
38 | 23, 37 | exbid 2221 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
39 | 22, 38 | pm2.61i 185 |
. . . 4
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)) |
40 | 39 | abbii 2808 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
41 | | df-opab 5116 |
. . 3
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} |
42 | | df-opab 5116 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
43 | 40, 41, 42 | 3eqtr4i 2775 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
44 | 1, 43 | eqtri 2765 |
1
⊢ I =
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |