Step | Hyp | Ref
| Expression |
1 | | df-id 5453 |
. 2
⊢ I =
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} |
2 | | equcom 2016 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
3 | 2 | anbi1ci 625 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
4 | 3 | exbii 1839 |
. . . . . . . . 9
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
5 | | opeq2 4796 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑥〉) |
6 | 5 | eqeq2d 2829 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑥〉)) |
7 | 6 | equsexvw 2002 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉) ↔ 𝑤 = 〈𝑥, 𝑥〉) |
8 | | equid 2010 |
. . . . . . . . . 10
⊢ 𝑥 = 𝑥 |
9 | 8 | biantru 530 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑥〉 ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
10 | 4, 7, 9 | 3bitri 298 |
. . . . . . . 8
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
11 | 10 | exbii 1839 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
12 | | nfe1 2145 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) |
13 | 12 | 19.9 2195 |
. . . . . . 7
⊢
(∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
14 | 11, 13 | bitr4i 279 |
. . . . . 6
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
15 | | opeq2 4796 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
16 | 15 | eqeq2d 2829 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑤 = 〈𝑥, 𝑥〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
17 | | equequ2 2024 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 ↔ 𝑥 = 𝑦)) |
18 | 16, 17 | anbi12d 630 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
19 | 18 | sps 2174 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
20 | 19 | drex1 2455 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
21 | 20 | drex2 2456 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
22 | 14, 21 | syl5bb 284 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
23 | | nfnae 2448 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
24 | | nfnae 2448 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
25 | | nfcvd 2975 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
26 | | nfcvf2 3005 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
27 | | nfcvd 2975 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑧) |
28 | 26, 27 | nfopd 4812 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦〈𝑥, 𝑧〉) |
29 | 25, 28 | nfeqd 2985 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = 〈𝑥, 𝑧〉) |
30 | 26, 27 | nfeqd 2985 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧) |
31 | 29, 30 | nfand 1889 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)) |
32 | | opeq2 4796 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑦〉) |
33 | 32 | eqeq2d 2829 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
34 | | equequ2 2024 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
35 | 33, 34 | anbi12d 630 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
36 | 35 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)))) |
37 | 24, 31, 36 | cbvexd 2420 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
38 | 23, 37 | exbid 2215 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
39 | 22, 38 | pm2.61i 183 |
. . . 4
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)) |
40 | 39 | abbii 2883 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
41 | | df-opab 5120 |
. . 3
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} |
42 | | df-opab 5120 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
43 | 40, 41, 42 | 3eqtr4i 2851 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
44 | 1, 43 | eqtri 2841 |
1
⊢ I =
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |