Step | Hyp | Ref
| Expression |
1 | | df-id 5575 |
. 2
⊢ I =
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} |
2 | | equcomi 2021 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
3 | 2 | opeq2d 4881 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑥⟩) |
4 | 3 | eqeq2d 2744 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩)) |
5 | 4 | pm5.32ri 577 |
. . . . . . . . 9
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦)) |
6 | 5 | exbii 1851 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦)) |
7 | | ax6evr 2019 |
. . . . . . . . 9
⊢
∃𝑦 𝑥 = 𝑦 |
8 | | 19.42v 1958 |
. . . . . . . . 9
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦) ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ ∃𝑦 𝑥 = 𝑦)) |
9 | 7, 8 | mpbiran2 709 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦) ↔ 𝑧 = ⟨𝑥, 𝑥⟩) |
10 | 6, 9 | bitri 275 |
. . . . . . 7
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ 𝑧 = ⟨𝑥, 𝑥⟩) |
11 | 10 | exbii 1851 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
12 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
13 | 12, 12 | opeq12d 4882 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ⟨𝑥, 𝑥⟩ = ⟨𝑢, 𝑢⟩) |
14 | 13 | eqeq2d 2744 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑥⟩ ↔ 𝑧 = ⟨𝑢, 𝑢⟩)) |
15 | 14 | exexw 2055 |
. . . . . 6
⊢
(∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
16 | 11, 15 | bitri 275 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
17 | | tru 1546 |
. . . . . . . 8
⊢
⊤ |
18 | 17 | biantru 531 |
. . . . . . 7
⊢ (𝑧 = ⟨𝑥, 𝑥⟩ ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
19 | 18 | exbii 1851 |
. . . . . 6
⊢
(∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
20 | 19 | exbii 1851 |
. . . . 5
⊢
(∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
21 | 16, 20 | bitri 275 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
22 | 21 | abbii 2803 |
. . 3
⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)} = {𝑧 ∣ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)} |
23 | | df-opab 5212 |
. . 3
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)} |
24 | | df-opab 5212 |
. . 3
⊢
{⟨𝑥, 𝑥⟩ ∣ ⊤} =
{𝑧 ∣ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)} |
25 | 22, 23, 24 | 3eqtr4i 2771 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {⟨𝑥, 𝑥⟩ ∣ ⊤} |
26 | 1, 25 | eqtri 2761 |
1
⊢ I =
{⟨𝑥, 𝑥⟩ ∣
⊤} |