Step | Hyp | Ref
| Expression |
1 | | df-id 5574 |
. 2
⊢ I =
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} |
2 | | equcomi 2020 |
. . . . . . . . . . . 12
⊢ (𝑥 = 𝑦 → 𝑦 = 𝑥) |
3 | 2 | opeq2d 4880 |
. . . . . . . . . . 11
⊢ (𝑥 = 𝑦 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑥⟩) |
4 | 3 | eqeq2d 2743 |
. . . . . . . . . 10
⊢ (𝑥 = 𝑦 → (𝑧 = ⟨𝑥, 𝑦⟩ ↔ 𝑧 = ⟨𝑥, 𝑥⟩)) |
5 | 4 | pm5.32ri 576 |
. . . . . . . . 9
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦)) |
6 | 5 | exbii 1850 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦)) |
7 | | ax6evr 2018 |
. . . . . . . . 9
⊢
∃𝑦 𝑥 = 𝑦 |
8 | | 19.42v 1957 |
. . . . . . . . 9
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦) ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ ∃𝑦 𝑥 = 𝑦)) |
9 | 7, 8 | mpbiran2 708 |
. . . . . . . 8
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑥⟩ ∧ 𝑥 = 𝑦) ↔ 𝑧 = ⟨𝑥, 𝑥⟩) |
10 | 6, 9 | bitri 274 |
. . . . . . 7
⊢
(∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ 𝑧 = ⟨𝑥, 𝑥⟩) |
11 | 10 | exbii 1850 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
12 | | id 22 |
. . . . . . . . 9
⊢ (𝑥 = 𝑢 → 𝑥 = 𝑢) |
13 | 12, 12 | opeq12d 4881 |
. . . . . . . 8
⊢ (𝑥 = 𝑢 → ⟨𝑥, 𝑥⟩ = ⟨𝑢, 𝑢⟩) |
14 | 13 | eqeq2d 2743 |
. . . . . . 7
⊢ (𝑥 = 𝑢 → (𝑧 = ⟨𝑥, 𝑥⟩ ↔ 𝑧 = ⟨𝑢, 𝑢⟩)) |
15 | 14 | exexw 2054 |
. . . . . 6
⊢
(∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
16 | 11, 15 | bitri 274 |
. . . . 5
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩) |
17 | | tru 1545 |
. . . . . . . 8
⊢
⊤ |
18 | 17 | biantru 530 |
. . . . . . 7
⊢ (𝑧 = ⟨𝑥, 𝑥⟩ ↔ (𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
19 | 18 | exbii 1850 |
. . . . . 6
⊢
(∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
20 | 19 | exbii 1850 |
. . . . 5
⊢
(∃𝑥∃𝑥 𝑧 = ⟨𝑥, 𝑥⟩ ↔ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
21 | 16, 20 | bitri 274 |
. . . 4
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦) ↔ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)) |
22 | 21 | abbii 2802 |
. . 3
⊢ {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)} = {𝑧 ∣ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)} |
23 | | df-opab 5211 |
. . 3
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝑥 = 𝑦)} |
24 | | df-opab 5211 |
. . 3
⊢
{⟨𝑥, 𝑥⟩ ∣ ⊤} =
{𝑧 ∣ ∃𝑥∃𝑥(𝑧 = ⟨𝑥, 𝑥⟩ ∧ ⊤)} |
25 | 22, 23, 24 | 3eqtr4i 2770 |
. 2
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝑥 = 𝑦} = {⟨𝑥, 𝑥⟩ ∣ ⊤} |
26 | 1, 25 | eqtri 2760 |
1
⊢ I =
{⟨𝑥, 𝑥⟩ ∣
⊤} |