Step | Hyp | Ref
| Expression |
1 | | sprsymrelf.f |
. 2
⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) |
2 | | sprsymrelfvlem 44911 |
. . . . 5
⊢ (𝑝 ⊆ (Pairs‘𝑉) → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉)) |
3 | | prcom 4674 |
. . . . . . . . . 10
⊢ {𝑥, 𝑦} = {𝑦, 𝑥} |
4 | 3 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑝 ⊆ (Pairs‘𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑝) → {𝑥, 𝑦} = {𝑦, 𝑥}) |
5 | 4 | eqeq2d 2751 |
. . . . . . . 8
⊢ (((𝑝 ⊆ (Pairs‘𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) ∧ 𝑐 ∈ 𝑝) → (𝑐 = {𝑥, 𝑦} ↔ 𝑐 = {𝑦, 𝑥})) |
6 | 5 | rexbidva 3227 |
. . . . . . 7
⊢ ((𝑝 ⊆ (Pairs‘𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑦, 𝑥})) |
7 | | df-br 5080 |
. . . . . . . 8
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) |
8 | | opabidw 5441 |
. . . . . . . 8
⊢
(〈𝑥, 𝑦〉 ∈ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}) |
9 | 7, 8 | bitri 274 |
. . . . . . 7
⊢ (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}) |
10 | | vex 3435 |
. . . . . . . 8
⊢ 𝑦 ∈ V |
11 | | vex 3435 |
. . . . . . . 8
⊢ 𝑥 ∈ V |
12 | | preq12 4677 |
. . . . . . . . . 10
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → {𝑎, 𝑏} = {𝑦, 𝑥}) |
13 | 12 | eqeq2d 2751 |
. . . . . . . . 9
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (𝑐 = {𝑎, 𝑏} ↔ 𝑐 = {𝑦, 𝑥})) |
14 | 13 | rexbidv 3228 |
. . . . . . . 8
⊢ ((𝑎 = 𝑦 ∧ 𝑏 = 𝑥) → (∃𝑐 ∈ 𝑝 𝑐 = {𝑎, 𝑏} ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑦, 𝑥})) |
15 | | preq12 4677 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → {𝑥, 𝑦} = {𝑎, 𝑏}) |
16 | 15 | eqeq2d 2751 |
. . . . . . . . . 10
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (𝑐 = {𝑥, 𝑦} ↔ 𝑐 = {𝑎, 𝑏})) |
17 | 16 | rexbidv 3228 |
. . . . . . . . 9
⊢ ((𝑥 = 𝑎 ∧ 𝑦 = 𝑏) → (∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑎, 𝑏})) |
18 | 17 | cbvopabv 5152 |
. . . . . . . 8
⊢
{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} = {〈𝑎, 𝑏〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑎, 𝑏}} |
19 | 10, 11, 14, 18 | braba 5453 |
. . . . . . 7
⊢ (𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥 ↔ ∃𝑐 ∈ 𝑝 𝑐 = {𝑦, 𝑥}) |
20 | 6, 9, 19 | 3bitr4g 314 |
. . . . . 6
⊢ ((𝑝 ⊆ (Pairs‘𝑉) ∧ (𝑥 ∈ 𝑉 ∧ 𝑦 ∈ 𝑉)) → (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥)) |
21 | 20 | ralrimivva 3117 |
. . . . 5
⊢ (𝑝 ⊆ (Pairs‘𝑉) → ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥)) |
22 | 2, 21 | jca 512 |
. . . 4
⊢ (𝑝 ⊆ (Pairs‘𝑉) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥))) |
23 | | sprsymrelf.p |
. . . . . 6
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) |
24 | 23 | eleq2i 2832 |
. . . . 5
⊢ (𝑝 ∈ 𝑃 ↔ 𝑝 ∈ 𝒫 (Pairs‘𝑉)) |
25 | | vex 3435 |
. . . . . 6
⊢ 𝑝 ∈ V |
26 | 25 | elpw 4543 |
. . . . 5
⊢ (𝑝 ∈ 𝒫
(Pairs‘𝑉) ↔
𝑝 ⊆
(Pairs‘𝑉)) |
27 | 24, 26 | bitri 274 |
. . . 4
⊢ (𝑝 ∈ 𝑃 ↔ 𝑝 ⊆ (Pairs‘𝑉)) |
28 | | nfopab1 5149 |
. . . . . . 7
⊢
Ⅎ𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} |
29 | 28 | nfeq2 2926 |
. . . . . 6
⊢
Ⅎ𝑥 𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} |
30 | | nfopab2 5150 |
. . . . . . . 8
⊢
Ⅎ𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} |
31 | 30 | nfeq2 2926 |
. . . . . . 7
⊢
Ⅎ𝑦 𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} |
32 | | breq 5081 |
. . . . . . . 8
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} → (𝑥𝑟𝑦 ↔ 𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦)) |
33 | | breq 5081 |
. . . . . . . 8
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} → (𝑦𝑟𝑥 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥)) |
34 | 32, 33 | bibi12d 346 |
. . . . . . 7
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} → ((𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥) ↔ (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥))) |
35 | 31, 34 | ralbid 3161 |
. . . . . 6
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} → (∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥) ↔ ∀𝑦 ∈ 𝑉 (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥))) |
36 | 29, 35 | ralbid 3161 |
. . . . 5
⊢ (𝑟 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥))) |
37 | 36 | elrab 3626 |
. . . 4
⊢
({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} ↔ ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑦 ↔ 𝑦{〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}𝑥))) |
38 | 22, 27, 37 | 3imtr4i 292 |
. . 3
⊢ (𝑝 ∈ 𝑃 → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)}) |
39 | | sprsymrelf.r |
. . 3
⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} |
40 | 38, 39 | eleqtrrdi 2852 |
. 2
⊢ (𝑝 ∈ 𝑃 → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}} ∈ 𝑅) |
41 | 1, 40 | fmpti 6983 |
1
⊢ 𝐹:𝑃⟶𝑅 |