Step | Hyp | Ref
| Expression |
1 | | relopabi.1 |
. . . . . . . 8
⊢ 𝐴 = {⟨𝑥, 𝑦⟩ ∣ 𝜑} |
2 | | df-opab 5173 |
. . . . . . . 8
⊢
{⟨𝑥, 𝑦⟩ ∣ 𝜑} = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} |
3 | 1, 2 | eqtri 2765 |
. . . . . . 7
⊢ 𝐴 = {𝑧 ∣ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)} |
4 | 3 | eqabi 2882 |
. . . . . 6
⊢ (𝑧 ∈ 𝐴 ↔ ∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑)) |
5 | | simpl 484 |
. . . . . . 7
⊢ ((𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → 𝑧 = ⟨𝑥, 𝑦⟩) |
6 | 5 | 2eximi 1839 |
. . . . . 6
⊢
(∃𝑥∃𝑦(𝑧 = ⟨𝑥, 𝑦⟩ ∧ 𝜑) → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) |
7 | 4, 6 | sylbi 216 |
. . . . 5
⊢ (𝑧 ∈ 𝐴 → ∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩) |
8 | | ax6evr 2019 |
. . . . . . . . . 10
⊢
∃𝑢 𝑦 = 𝑢 |
9 | | pm3.21 473 |
. . . . . . . . . . 11
⊢
(⟨𝑥, 𝑦⟩ = 𝑧 → (𝑦 = 𝑢 → (𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))) |
10 | 9 | eximdv 1921 |
. . . . . . . . . 10
⊢
(⟨𝑥, 𝑦⟩ = 𝑧 → (∃𝑢 𝑦 = 𝑢 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧))) |
11 | 8, 10 | mpi 20 |
. . . . . . . . 9
⊢
(⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧)) |
12 | | opeq2 4836 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑢 → ⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩) |
13 | | eqtr2 2761 |
. . . . . . . . . . . 12
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ⟨𝑥, 𝑢⟩ = 𝑧) |
14 | 13 | eqcomd 2743 |
. . . . . . . . . . 11
⊢
((⟨𝑥, 𝑦⟩ = ⟨𝑥, 𝑢⟩ ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩) |
15 | 12, 14 | sylan 581 |
. . . . . . . . . 10
⊢ ((𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → 𝑧 = ⟨𝑥, 𝑢⟩) |
16 | 15 | eximi 1838 |
. . . . . . . . 9
⊢
(∃𝑢(𝑦 = 𝑢 ∧ ⟨𝑥, 𝑦⟩ = 𝑧) → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
17 | 11, 16 | syl 17 |
. . . . . . . 8
⊢
(⟨𝑥, 𝑦⟩ = 𝑧 → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
18 | 17 | eqcoms 2745 |
. . . . . . 7
⊢ (𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
19 | 18 | 2eximi 1839 |
. . . . . 6
⊢
(∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑥∃𝑦∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
20 | | excomim 2164 |
. . . . . 6
⊢
(∃𝑥∃𝑦∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
21 | 19, 20 | syl 17 |
. . . . 5
⊢
(∃𝑥∃𝑦 𝑧 = ⟨𝑥, 𝑦⟩ → ∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩) |
22 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑥 ∈ V |
23 | | vex 3452 |
. . . . . . . . . 10
⊢ 𝑢 ∈ V |
24 | 22, 23 | pm3.2i 472 |
. . . . . . . . 9
⊢ (𝑥 ∈ V ∧ 𝑢 ∈ V) |
25 | 24 | jctr 526 |
. . . . . . . 8
⊢ (𝑧 = ⟨𝑥, 𝑢⟩ → (𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))) |
26 | 25 | 2eximi 1839 |
. . . . . . 7
⊢
(∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))) |
27 | | df-xp 5644 |
. . . . . . . . 9
⊢ (V
× V) = {⟨𝑥,
𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} |
28 | | df-opab 5173 |
. . . . . . . . 9
⊢
{⟨𝑥, 𝑢⟩ ∣ (𝑥 ∈ V ∧ 𝑢 ∈ V)} = {𝑧 ∣ ∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))} |
29 | 27, 28 | eqtri 2765 |
. . . . . . . 8
⊢ (V
× V) = {𝑧 ∣
∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))} |
30 | 29 | eqabi 2882 |
. . . . . . 7
⊢ (𝑧 ∈ (V × V) ↔
∃𝑥∃𝑢(𝑧 = ⟨𝑥, 𝑢⟩ ∧ (𝑥 ∈ V ∧ 𝑢 ∈ V))) |
31 | 26, 30 | sylibr 233 |
. . . . . 6
⊢
(∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → 𝑧 ∈ (V × V)) |
32 | 31 | eximi 1838 |
. . . . 5
⊢
(∃𝑦∃𝑥∃𝑢 𝑧 = ⟨𝑥, 𝑢⟩ → ∃𝑦 𝑧 ∈ (V × V)) |
33 | 7, 21, 32 | 3syl 18 |
. . . 4
⊢ (𝑧 ∈ 𝐴 → ∃𝑦 𝑧 ∈ (V × V)) |
34 | | ax5e 1916 |
. . . 4
⊢
(∃𝑦 𝑧 ∈ (V × V) →
𝑧 ∈ (V ×
V)) |
35 | 33, 34 | syl 17 |
. . 3
⊢ (𝑧 ∈ 𝐴 → 𝑧 ∈ (V × V)) |
36 | 35 | ssriv 3953 |
. 2
⊢ 𝐴 ⊆ (V ×
V) |
37 | | df-rel 5645 |
. 2
⊢ (Rel
𝐴 ↔ 𝐴 ⊆ (V × V)) |
38 | 36, 37 | mpbir 230 |
1
⊢ Rel 𝐴 |