Step | Hyp | Ref
| Expression |
1 | | sprsymrelf.p |
. . . 4
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) |
2 | | sprsymrelf.r |
. . . 4
⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} |
3 | | sprsymrelf.f |
. . . 4
⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) |
4 | 1, 2, 3 | sprsymrelf 44947 |
. . 3
⊢ 𝐹:𝑃⟶𝑅 |
5 | 4 | a1i 11 |
. 2
⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃⟶𝑅) |
6 | | breq 5076 |
. . . . . . . . 9
⊢ (𝑟 = 𝑡 → (𝑥𝑟𝑦 ↔ 𝑥𝑡𝑦)) |
7 | | breq 5076 |
. . . . . . . . 9
⊢ (𝑟 = 𝑡 → (𝑦𝑟𝑥 ↔ 𝑦𝑡𝑥)) |
8 | 6, 7 | bibi12d 346 |
. . . . . . . 8
⊢ (𝑟 = 𝑡 → ((𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥) ↔ (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥))) |
9 | 8 | 2ralbidv 3129 |
. . . . . . 7
⊢ (𝑟 = 𝑡 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥) ↔ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥))) |
10 | 9, 2 | elrab2 3627 |
. . . . . 6
⊢ (𝑡 ∈ 𝑅 ↔ (𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥))) |
11 | | eqid 2738 |
. . . . . . . . . . 11
⊢ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} |
12 | 11 | sprsymrelfolem1 44944 |
. . . . . . . . . 10
⊢ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} ∈ 𝒫 (Pairs‘𝑉) |
13 | 12, 1 | eleqtrri 2838 |
. . . . . . . . 9
⊢ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} ∈ 𝑃 |
14 | 13 | a1i 11 |
. . . . . . . 8
⊢ (((𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) ∧ 𝑉 ∈ 𝑊) → {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} ∈ 𝑃) |
15 | | rexeq 3343 |
. . . . . . . . . . 11
⊢ (𝑓 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} → (∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦} ↔ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦})) |
16 | 15 | opabbidv 5140 |
. . . . . . . . . 10
⊢ (𝑓 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} → {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}) |
17 | 16 | eqeq2d 2749 |
. . . . . . . . 9
⊢ (𝑓 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)} → (𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}} ↔ 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}})) |
18 | 17 | adantl 482 |
. . . . . . . 8
⊢ ((((𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) ∧ 𝑉 ∈ 𝑊) ∧ 𝑓 = {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}) → (𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}} ↔ 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}})) |
19 | | velpw 4538 |
. . . . . . . . . 10
⊢ (𝑡 ∈ 𝒫 (𝑉 × 𝑉) ↔ 𝑡 ⊆ (𝑉 × 𝑉)) |
20 | | xpss 5605 |
. . . . . . . . . . . . . . . 16
⊢ (𝑉 × 𝑉) ⊆ (V × V) |
21 | | sstr2 3928 |
. . . . . . . . . . . . . . . 16
⊢ (𝑡 ⊆ (𝑉 × 𝑉) → ((𝑉 × 𝑉) ⊆ (V × V) → 𝑡 ⊆ (V ×
V))) |
22 | 20, 21 | mpi 20 |
. . . . . . . . . . . . . . 15
⊢ (𝑡 ⊆ (𝑉 × 𝑉) → 𝑡 ⊆ (V × V)) |
23 | | df-rel 5596 |
. . . . . . . . . . . . . . 15
⊢ (Rel
𝑡 ↔ 𝑡 ⊆ (V × V)) |
24 | 22, 23 | sylibr 233 |
. . . . . . . . . . . . . 14
⊢ (𝑡 ⊆ (𝑉 × 𝑉) → Rel 𝑡) |
25 | 24 | adantl 482 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) → Rel 𝑡) |
26 | | dfrel4v 6093 |
. . . . . . . . . . . . . 14
⊢ (Rel
𝑡 ↔ 𝑡 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦}) |
27 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥(𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) |
28 | | nfra1 3144 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑥∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) |
29 | 27, 28 | nfan 1902 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑥((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) |
30 | | nfv 1917 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦(𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) |
31 | | nfra2w 3154 |
. . . . . . . . . . . . . . . . . . . 20
⊢
Ⅎ𝑦∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) |
32 | 30, 31 | nfan 1902 |
. . . . . . . . . . . . . . . . . . 19
⊢
Ⅎ𝑦((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) |
33 | 11 | sprsymrelfolem2 44945 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → (𝑥𝑡𝑦 ↔ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦})) |
34 | 33 | 3expa 1117 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → (𝑥𝑡𝑦 ↔ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦})) |
35 | 29, 32, 34 | opabbid 5139 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}) |
36 | 35 | eqeq2d 2749 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → (𝑡 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦} ↔ 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}})) |
37 | 36 | biimpd 228 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → (𝑡 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦} → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}})) |
38 | 37 | ex 413 |
. . . . . . . . . . . . . . 15
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → (𝑡 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦} → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
39 | 38 | com23 86 |
. . . . . . . . . . . . . 14
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) → (𝑡 = {〈𝑥, 𝑦〉 ∣ 𝑥𝑡𝑦} → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
40 | 26, 39 | syl5bi 241 |
. . . . . . . . . . . . 13
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) → (Rel 𝑡 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
41 | 25, 40 | mpd 15 |
. . . . . . . . . . . 12
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ⊆ (𝑉 × 𝑉)) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}})) |
42 | 41 | expcom 414 |
. . . . . . . . . . 11
⊢ (𝑡 ⊆ (𝑉 × 𝑉) → (𝑉 ∈ 𝑊 → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
43 | 42 | com23 86 |
. . . . . . . . . 10
⊢ (𝑡 ⊆ (𝑉 × 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → (𝑉 ∈ 𝑊 → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
44 | 19, 43 | sylbi 216 |
. . . . . . . . 9
⊢ (𝑡 ∈ 𝒫 (𝑉 × 𝑉) → (∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥) → (𝑉 ∈ 𝑊 → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}))) |
45 | 44 | imp31 418 |
. . . . . . . 8
⊢ (((𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) ∧ 𝑉 ∈ 𝑊) → 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ {𝑞 ∈ (Pairs‘𝑉) ∣ ∀𝑎 ∈ 𝑉 ∀𝑏 ∈ 𝑉 (𝑞 = {𝑎, 𝑏} → 𝑎𝑡𝑏)}𝑐 = {𝑥, 𝑦}}) |
46 | 14, 18, 45 | rspcedvd 3563 |
. . . . . . 7
⊢ (((𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) ∧ 𝑉 ∈ 𝑊) → ∃𝑓 ∈ 𝑃 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}}) |
47 | 46 | ex 413 |
. . . . . 6
⊢ ((𝑡 ∈ 𝒫 (𝑉 × 𝑉) ∧ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑡𝑦 ↔ 𝑦𝑡𝑥)) → (𝑉 ∈ 𝑊 → ∃𝑓 ∈ 𝑃 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}})) |
48 | 10, 47 | sylbi 216 |
. . . . 5
⊢ (𝑡 ∈ 𝑅 → (𝑉 ∈ 𝑊 → ∃𝑓 ∈ 𝑃 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}})) |
49 | 48 | impcom 408 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅) → ∃𝑓 ∈ 𝑃 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}}) |
50 | 1, 2, 3 | sprsymrelfv 44946 |
. . . . . . 7
⊢ (𝑓 ∈ 𝑃 → (𝐹‘𝑓) = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}}) |
51 | 50 | adantl 482 |
. . . . . 6
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅) ∧ 𝑓 ∈ 𝑃) → (𝐹‘𝑓) = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}}) |
52 | 51 | eqeq2d 2749 |
. . . . 5
⊢ (((𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅) ∧ 𝑓 ∈ 𝑃) → (𝑡 = (𝐹‘𝑓) ↔ 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}})) |
53 | 52 | rexbidva 3225 |
. . . 4
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅) → (∃𝑓 ∈ 𝑃 𝑡 = (𝐹‘𝑓) ↔ ∃𝑓 ∈ 𝑃 𝑡 = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑓 𝑐 = {𝑥, 𝑦}})) |
54 | 49, 53 | mpbird 256 |
. . 3
⊢ ((𝑉 ∈ 𝑊 ∧ 𝑡 ∈ 𝑅) → ∃𝑓 ∈ 𝑃 𝑡 = (𝐹‘𝑓)) |
55 | 54 | ralrimiva 3103 |
. 2
⊢ (𝑉 ∈ 𝑊 → ∀𝑡 ∈ 𝑅 ∃𝑓 ∈ 𝑃 𝑡 = (𝐹‘𝑓)) |
56 | | dffo3 6978 |
. 2
⊢ (𝐹:𝑃–onto→𝑅 ↔ (𝐹:𝑃⟶𝑅 ∧ ∀𝑡 ∈ 𝑅 ∃𝑓 ∈ 𝑃 𝑡 = (𝐹‘𝑓))) |
57 | 5, 55, 56 | sylanbrc 583 |
1
⊢ (𝑉 ∈ 𝑊 → 𝐹:𝑃–onto→𝑅) |