| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | sprsymrelf.p | . . 3
⊢ 𝑃 = 𝒫 (Pairs‘𝑉) | 
| 2 |  | sprsymrelf.r | . . 3
⊢ 𝑅 = {𝑟 ∈ 𝒫 (𝑉 × 𝑉) ∣ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (𝑥𝑟𝑦 ↔ 𝑦𝑟𝑥)} | 
| 3 |  | sprsymrelf.f | . . 3
⊢ 𝐹 = (𝑝 ∈ 𝑃 ↦ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑝 𝑐 = {𝑥, 𝑦}}) | 
| 4 | 1, 2, 3 | sprsymrelf 47482 | . 2
⊢ 𝐹:𝑃⟶𝑅 | 
| 5 | 1, 2, 3 | sprsymrelfv 47481 | . . . . 5
⊢ (𝑎 ∈ 𝑃 → (𝐹‘𝑎) = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}}) | 
| 6 | 1, 2, 3 | sprsymrelfv 47481 | . . . . 5
⊢ (𝑏 ∈ 𝑃 → (𝐹‘𝑏) = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}}) | 
| 7 | 5, 6 | eqeqan12d 2751 | . . . 4
⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝐹‘𝑎) = (𝐹‘𝑏) ↔ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}})) | 
| 8 | 1 | eleq2i 2833 | . . . . . 6
⊢ (𝑎 ∈ 𝑃 ↔ 𝑎 ∈ 𝒫 (Pairs‘𝑉)) | 
| 9 |  | vex 3484 | . . . . . . 7
⊢ 𝑎 ∈ V | 
| 10 | 9 | elpw 4604 | . . . . . 6
⊢ (𝑎 ∈ 𝒫
(Pairs‘𝑉) ↔
𝑎 ⊆
(Pairs‘𝑉)) | 
| 11 | 8, 10 | bitri 275 | . . . . 5
⊢ (𝑎 ∈ 𝑃 ↔ 𝑎 ⊆ (Pairs‘𝑉)) | 
| 12 | 1 | eleq2i 2833 | . . . . . 6
⊢ (𝑏 ∈ 𝑃 ↔ 𝑏 ∈ 𝒫 (Pairs‘𝑉)) | 
| 13 |  | vex 3484 | . . . . . . 7
⊢ 𝑏 ∈ V | 
| 14 | 13 | elpw 4604 | . . . . . 6
⊢ (𝑏 ∈ 𝒫
(Pairs‘𝑉) ↔
𝑏 ⊆
(Pairs‘𝑉)) | 
| 15 | 12, 14 | bitri 275 | . . . . 5
⊢ (𝑏 ∈ 𝑃 ↔ 𝑏 ⊆ (Pairs‘𝑉)) | 
| 16 |  | sprsymrelf1lem 47478 | . . . . . . . 8
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 ⊆ 𝑏)) | 
| 17 | 16 | imp 406 | . . . . . . 7
⊢ (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}}) → 𝑎 ⊆ 𝑏) | 
| 18 |  | eqcom 2744 | . . . . . . . . . 10
⊢
({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} ↔ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}}) | 
| 19 |  | sprsymrelf1lem 47478 | . . . . . . . . . 10
⊢ ((𝑏 ⊆ (Pairs‘𝑉) ∧ 𝑎 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} → 𝑏 ⊆ 𝑎)) | 
| 20 | 18, 19 | biimtrid 242 | . . . . . . . . 9
⊢ ((𝑏 ⊆ (Pairs‘𝑉) ∧ 𝑎 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑏 ⊆ 𝑎)) | 
| 21 | 20 | ancoms 458 | . . . . . . . 8
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑏 ⊆ 𝑎)) | 
| 22 | 21 | imp 406 | . . . . . . 7
⊢ (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}}) → 𝑏 ⊆ 𝑎) | 
| 23 | 17, 22 | eqssd 4001 | . . . . . 6
⊢ (((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) ∧ {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}}) → 𝑎 = 𝑏) | 
| 24 | 23 | ex 412 | . . . . 5
⊢ ((𝑎 ⊆ (Pairs‘𝑉) ∧ 𝑏 ⊆ (Pairs‘𝑉)) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 = 𝑏)) | 
| 25 | 11, 15, 24 | syl2anb 598 | . . . 4
⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ({〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑎 𝑐 = {𝑥, 𝑦}} = {〈𝑥, 𝑦〉 ∣ ∃𝑐 ∈ 𝑏 𝑐 = {𝑥, 𝑦}} → 𝑎 = 𝑏)) | 
| 26 | 7, 25 | sylbid 240 | . . 3
⊢ ((𝑎 ∈ 𝑃 ∧ 𝑏 ∈ 𝑃) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) | 
| 27 | 26 | rgen2 3199 | . 2
⊢
∀𝑎 ∈
𝑃 ∀𝑏 ∈ 𝑃 ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏) | 
| 28 |  | dff13 7275 | . 2
⊢ (𝐹:𝑃–1-1→𝑅 ↔ (𝐹:𝑃⟶𝑅 ∧ ∀𝑎 ∈ 𝑃 ∀𝑏 ∈ 𝑃 ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏))) | 
| 29 | 4, 27, 28 | mpbir2an 711 | 1
⊢ 𝐹:𝑃–1-1→𝑅 |