| Step | Hyp | Ref
| Expression |
| 1 | | df-id 5576 |
. 2
⊢ I =
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} |
| 2 | | equcom 2017 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑧 ↔ 𝑧 = 𝑥) |
| 3 | 2 | anbi1ci 626 |
. . . . . . . . . 10
⊢ ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
| 4 | 3 | exbii 1848 |
. . . . . . . . 9
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉)) |
| 5 | | opeq2 4872 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑥 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑥〉) |
| 6 | 5 | eqeq2d 2747 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑥 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑥〉)) |
| 7 | 6 | equsexvw 2004 |
. . . . . . . . 9
⊢
(∃𝑧(𝑧 = 𝑥 ∧ 𝑤 = 〈𝑥, 𝑧〉) ↔ 𝑤 = 〈𝑥, 𝑥〉) |
| 8 | | equid 2011 |
. . . . . . . . . 10
⊢ 𝑥 = 𝑥 |
| 9 | 8 | biantru 529 |
. . . . . . . . 9
⊢ (𝑤 = 〈𝑥, 𝑥〉 ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
| 10 | 4, 7, 9 | 3bitri 297 |
. . . . . . . 8
⊢
(∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
| 11 | 10 | exbii 1848 |
. . . . . . 7
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
| 12 | | nfe1 2150 |
. . . . . . . 8
⊢
Ⅎ𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) |
| 13 | 12 | 19.9 2205 |
. . . . . . 7
⊢
(∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
| 14 | 11, 13 | bitr4i 278 |
. . . . . 6
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥)) |
| 15 | | opeq2 4872 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → 〈𝑥, 𝑥〉 = 〈𝑥, 𝑦〉) |
| 16 | 15 | eqeq2d 2747 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑤 = 〈𝑥, 𝑥〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
| 17 | | equequ2 2025 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑥 = 𝑥 ↔ 𝑥 = 𝑦)) |
| 18 | 16, 17 | anbi12d 632 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 19 | 18 | sps 2185 |
. . . . . . . 8
⊢
(∀𝑥 𝑥 = 𝑦 → ((𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 20 | 19 | drex1 2445 |
. . . . . . 7
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 21 | 20 | drex2 2446 |
. . . . . 6
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑥(𝑤 = 〈𝑥, 𝑥〉 ∧ 𝑥 = 𝑥) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 22 | 14, 21 | bitrid 283 |
. . . . 5
⊢
(∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 23 | | nfnae 2438 |
. . . . . 6
⊢
Ⅎ𝑥 ¬
∀𝑥 𝑥 = 𝑦 |
| 24 | | nfnae 2438 |
. . . . . . 7
⊢
Ⅎ𝑦 ¬
∀𝑥 𝑥 = 𝑦 |
| 25 | | nfcvd 2905 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑤) |
| 26 | | nfcvf2 2932 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑥) |
| 27 | | nfcvd 2905 |
. . . . . . . . . 10
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦𝑧) |
| 28 | 26, 27 | nfopd 4888 |
. . . . . . . . 9
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦〈𝑥, 𝑧〉) |
| 29 | 25, 28 | nfeqd 2915 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑤 = 〈𝑥, 𝑧〉) |
| 30 | 26, 27 | nfeqd 2915 |
. . . . . . . 8
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦 𝑥 = 𝑧) |
| 31 | 29, 30 | nfand 1897 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → Ⅎ𝑦(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)) |
| 32 | | opeq2 4872 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑦 → 〈𝑥, 𝑧〉 = 〈𝑥, 𝑦〉) |
| 33 | 32 | eqeq2d 2747 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑤 = 〈𝑥, 𝑧〉 ↔ 𝑤 = 〈𝑥, 𝑦〉)) |
| 34 | | equequ2 2025 |
. . . . . . . . 9
⊢ (𝑧 = 𝑦 → (𝑥 = 𝑧 ↔ 𝑥 = 𝑦)) |
| 35 | 33, 34 | anbi12d 632 |
. . . . . . . 8
⊢ (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 36 | 35 | a1i 11 |
. . . . . . 7
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (𝑧 = 𝑦 → ((𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ (𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)))) |
| 37 | 24, 31, 36 | cbvexd 2412 |
. . . . . 6
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 38 | 23, 37 | exbid 2223 |
. . . . 5
⊢ (¬
∀𝑥 𝑥 = 𝑦 → (∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦))) |
| 39 | 22, 38 | pm2.61i 182 |
. . . 4
⊢
(∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧) ↔ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)) |
| 40 | 39 | abbii 2808 |
. . 3
⊢ {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
| 41 | | df-opab 5204 |
. . 3
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {𝑤 ∣ ∃𝑥∃𝑧(𝑤 = 〈𝑥, 𝑧〉 ∧ 𝑥 = 𝑧)} |
| 42 | | df-opab 5204 |
. . 3
⊢
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} = {𝑤 ∣ ∃𝑥∃𝑦(𝑤 = 〈𝑥, 𝑦〉 ∧ 𝑥 = 𝑦)} |
| 43 | 40, 41, 42 | 3eqtr4i 2774 |
. 2
⊢
{〈𝑥, 𝑧〉 ∣ 𝑥 = 𝑧} = {〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |
| 44 | 1, 43 | eqtri 2764 |
1
⊢ I =
{〈𝑥, 𝑦〉 ∣ 𝑥 = 𝑦} |