| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | funfvop 7070 | . . 3
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → 〈𝑋, (𝐹‘𝑋)〉 ∈ 𝐹) | 
| 2 |  | simplll 775 | . . . . . . . 8
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → Fun 𝐹) | 
| 3 |  | funrel 6583 | . . . . . . . 8
⊢ (Fun
𝐹 → Rel 𝐹) | 
| 4 | 2, 3 | syl 17 | . . . . . . 7
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → Rel 𝐹) | 
| 5 |  | simplr 769 | . . . . . . 7
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑝 ∈ 𝐹) | 
| 6 |  | 1st2nd 8064 | . . . . . . 7
⊢ ((Rel
𝐹 ∧ 𝑝 ∈ 𝐹) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) | 
| 7 | 4, 5, 6 | syl2anc 584 | . . . . . 6
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑝 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) | 
| 8 |  | simpr 484 | . . . . . . 7
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑋 = (1st ‘𝑝)) | 
| 9 |  | simpllr 776 | . . . . . . . 8
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑋 ∈ dom 𝐹) | 
| 10 | 8 | opeq1d 4879 | . . . . . . . . . 10
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 〈𝑋, (2nd ‘𝑝)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) | 
| 11 | 7, 10 | eqtr4d 2780 | . . . . . . . . 9
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑝 = 〈𝑋, (2nd ‘𝑝)〉) | 
| 12 | 11, 5 | eqeltrrd 2842 | . . . . . . . 8
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 〈𝑋, (2nd ‘𝑝)〉 ∈ 𝐹) | 
| 13 |  | funopfvb 6963 | . . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → ((𝐹‘𝑋) = (2nd ‘𝑝) ↔ 〈𝑋, (2nd ‘𝑝)〉 ∈ 𝐹)) | 
| 14 | 13 | biimpar 477 | . . . . . . . 8
⊢ (((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 〈𝑋, (2nd ‘𝑝)〉 ∈ 𝐹) → (𝐹‘𝑋) = (2nd ‘𝑝)) | 
| 15 | 2, 9, 12, 14 | syl21anc 838 | . . . . . . 7
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → (𝐹‘𝑋) = (2nd ‘𝑝)) | 
| 16 | 8, 15 | opeq12d 4881 | . . . . . 6
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 〈𝑋, (𝐹‘𝑋)〉 = 〈(1st ‘𝑝), (2nd ‘𝑝)〉) | 
| 17 | 7, 16 | eqtr4d 2780 | . . . . 5
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑋 = (1st ‘𝑝)) → 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) | 
| 18 |  | simpr 484 | . . . . . . 7
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) → 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) | 
| 19 | 18 | fveq2d 6910 | . . . . . 6
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) → (1st ‘𝑝) = (1st
‘〈𝑋, (𝐹‘𝑋)〉)) | 
| 20 |  | fvex 6919 | . . . . . . . 8
⊢ (𝐹‘𝑋) ∈ V | 
| 21 |  | op1stg 8026 | . . . . . . . 8
⊢ ((𝑋 ∈ dom 𝐹 ∧ (𝐹‘𝑋) ∈ V) → (1st
‘〈𝑋, (𝐹‘𝑋)〉) = 𝑋) | 
| 22 | 20, 21 | mpan2 691 | . . . . . . 7
⊢ (𝑋 ∈ dom 𝐹 → (1st ‘〈𝑋, (𝐹‘𝑋)〉) = 𝑋) | 
| 23 | 22 | ad3antlr 731 | . . . . . 6
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) → (1st
‘〈𝑋, (𝐹‘𝑋)〉) = 𝑋) | 
| 24 | 19, 23 | eqtr2d 2778 | . . . . 5
⊢ ((((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) ∧ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉) → 𝑋 = (1st ‘𝑝)) | 
| 25 | 17, 24 | impbida 801 | . . . 4
⊢ (((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) ∧ 𝑝 ∈ 𝐹) → (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉)) | 
| 26 | 25 | ralrimiva 3146 | . . 3
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉)) | 
| 27 |  | eqeq2 2749 | . . . . . 6
⊢ (𝑞 = 〈𝑋, (𝐹‘𝑋)〉 → (𝑝 = 𝑞 ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉)) | 
| 28 | 27 | bibi2d 342 | . . . . 5
⊢ (𝑞 = 〈𝑋, (𝐹‘𝑋)〉 → ((𝑋 = (1st ‘𝑝) ↔ 𝑝 = 𝑞) ↔ (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉))) | 
| 29 | 28 | ralbidv 3178 | . . . 4
⊢ (𝑞 = 〈𝑋, (𝐹‘𝑋)〉 → (∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 𝑞) ↔ ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉))) | 
| 30 | 29 | rspcev 3622 | . . 3
⊢
((〈𝑋, (𝐹‘𝑋)〉 ∈ 𝐹 ∧ ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 〈𝑋, (𝐹‘𝑋)〉)) → ∃𝑞 ∈ 𝐹 ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 𝑞)) | 
| 31 | 1, 26, 30 | syl2anc 584 | . 2
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃𝑞 ∈ 𝐹 ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 𝑞)) | 
| 32 |  | reu6 3732 | . 2
⊢
(∃!𝑝 ∈
𝐹 𝑋 = (1st ‘𝑝) ↔ ∃𝑞 ∈ 𝐹 ∀𝑝 ∈ 𝐹 (𝑋 = (1st ‘𝑝) ↔ 𝑝 = 𝑞)) | 
| 33 | 31, 32 | sylibr 234 | 1
⊢ ((Fun
𝐹 ∧ 𝑋 ∈ dom 𝐹) → ∃!𝑝 ∈ 𝐹 𝑋 = (1st ‘𝑝)) |