| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fundmen.1 | . . . 4
⊢ 𝐹 ∈ V | 
| 2 | 1 | dmex 7931 | . . 3
⊢ dom 𝐹 ∈ V | 
| 3 | 2 | a1i 11 | . 2
⊢ (Fun
𝐹 → dom 𝐹 ∈ V) | 
| 4 | 1 | a1i 11 | . 2
⊢ (Fun
𝐹 → 𝐹 ∈ V) | 
| 5 |  | funfvop 7070 | . . 3
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) | 
| 6 | 5 | ex 412 | . 2
⊢ (Fun
𝐹 → (𝑥 ∈ dom 𝐹 → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹)) | 
| 7 |  | funrel 6583 | . . 3
⊢ (Fun
𝐹 → Rel 𝐹) | 
| 8 |  | elreldm 5946 | . . . 4
⊢ ((Rel
𝐹 ∧ 𝑦 ∈ 𝐹) → ∩ ∩ 𝑦
∈ dom 𝐹) | 
| 9 | 8 | ex 412 | . . 3
⊢ (Rel
𝐹 → (𝑦 ∈ 𝐹 → ∩ ∩ 𝑦
∈ dom 𝐹)) | 
| 10 | 7, 9 | syl 17 | . 2
⊢ (Fun
𝐹 → (𝑦 ∈ 𝐹 → ∩ ∩ 𝑦
∈ dom 𝐹)) | 
| 11 |  | df-rel 5692 | . . . . . . . . 9
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) | 
| 12 | 7, 11 | sylib 218 | . . . . . . . 8
⊢ (Fun
𝐹 → 𝐹 ⊆ (V × V)) | 
| 13 | 12 | sselda 3983 | . . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → 𝑦 ∈ (V × V)) | 
| 14 |  | elvv 5760 | . . . . . . 7
⊢ (𝑦 ∈ (V × V) ↔
∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉) | 
| 15 | 13, 14 | sylib 218 | . . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → ∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉) | 
| 16 |  | inteq 4949 | . . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
𝑦 = ∩ 〈𝑧, 𝑤〉) | 
| 17 | 16 | inteqd 4951 | . . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑧, 𝑤〉) | 
| 18 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V | 
| 19 |  | vex 3484 | . . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V | 
| 20 | 18, 19 | op1stb 5476 | . . . . . . . . . . . . . . . 16
⊢ ∩ ∩ 〈𝑧, 𝑤〉 = 𝑧 | 
| 21 | 17, 20 | eqtrdi 2793 | . . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
∩ 𝑦 = 𝑧) | 
| 22 |  | eqeq1 2741 | . . . . . . . . . . . . . . 15
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑥 = 𝑧 ↔ ∩ ∩ 𝑦 =
𝑧)) | 
| 23 | 21, 22 | imbitrrid 246 | . . . . . . . . . . . . . 14
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → 𝑥 = 𝑧)) | 
| 24 |  | opeq1 4873 | . . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) | 
| 25 | 23, 24 | syl6 35 | . . . . . . . . . . . . 13
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉)) | 
| 26 | 25 | imp 406 | . . . . . . . . . . . 12
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) | 
| 27 |  | eqeq2 2749 | . . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → (𝑦 = 〈𝑥, 𝑤〉 ↔ 𝑦 = 〈𝑧, 𝑤〉)) | 
| 28 | 27 | biimprcd 250 | . . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → 𝑦 = 〈𝑥, 𝑤〉)) | 
| 29 | 28 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → (〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → 𝑦 = 〈𝑥, 𝑤〉)) | 
| 30 | 26, 29 | mpd 15 | . . . . . . . . . . 11
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → 𝑦 = 〈𝑥, 𝑤〉) | 
| 31 | 30 | ancoms 458 | . . . . . . . . . 10
⊢ ((𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦)
→ 𝑦 = 〈𝑥, 𝑤〉) | 
| 32 | 31 | adantl 481 | . . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 𝑦 = 〈𝑥, 𝑤〉) | 
| 33 | 30 | eleq1d 2826 | . . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → (𝑦 ∈ 𝐹 ↔ 〈𝑥, 𝑤〉 ∈ 𝐹)) | 
| 34 | 33 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (𝑦 ∈ 𝐹 ↔ 〈𝑥, 𝑤〉 ∈ 𝐹)) | 
| 35 |  | funopfv 6958 | . . . . . . . . . . . . . . 15
⊢ (Fun
𝐹 → (〈𝑥, 𝑤〉 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) | 
| 36 | 35 | adantr 480 | . . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (〈𝑥, 𝑤〉 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) | 
| 37 | 34, 36 | sylbid 240 | . . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (𝑦 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) | 
| 38 | 37 | exp32 420 | . . . . . . . . . . . 12
⊢ (Fun
𝐹 → (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)))) | 
| 39 | 38 | com24 95 | . . . . . . . . . . 11
⊢ (Fun
𝐹 → (𝑦 ∈ 𝐹 → (𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ (𝐹‘𝑥) = 𝑤)))) | 
| 40 | 39 | imp43 427 | . . . . . . . . . 10
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ (𝐹‘𝑥) = 𝑤) | 
| 41 | 40 | opeq2d 4880 | . . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 〈𝑥, (𝐹‘𝑥)〉 = 〈𝑥, 𝑤〉) | 
| 42 | 32, 41 | eqtr4d 2780 | . . . . . . . 8
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉) | 
| 43 | 42 | exp32 420 | . . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) | 
| 44 | 43 | exlimdvv 1934 | . . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) | 
| 45 | 15, 44 | mpd 15 | . . . . 5
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) | 
| 46 | 45 | adantrl 716 | . . . 4
⊢ ((Fun
𝐹 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) | 
| 47 |  | inteq 4949 | . . . . . 6
⊢ (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → ∩
𝑦 = ∩ 〈𝑥, (𝐹‘𝑥)〉) | 
| 48 | 47 | inteqd 4951 | . . . . 5
⊢ (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉) | 
| 49 |  | vex 3484 | . . . . . 6
⊢ 𝑥 ∈ V | 
| 50 |  | fvex 6919 | . . . . . 6
⊢ (𝐹‘𝑥) ∈ V | 
| 51 | 49, 50 | op1stb 5476 | . . . . 5
⊢ ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉 = 𝑥 | 
| 52 | 48, 51 | eqtr2di 2794 | . . . 4
⊢ (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → 𝑥 = ∩ ∩ 𝑦) | 
| 53 | 46, 52 | impbid1 225 | . . 3
⊢ ((Fun
𝐹 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 = ∩ ∩ 𝑦
↔ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) | 
| 54 | 53 | ex 412 | . 2
⊢ (Fun
𝐹 → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 = ∩ ∩ 𝑦
↔ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) | 
| 55 | 3, 4, 6, 10, 54 | en3d 9029 | 1
⊢ (Fun
𝐹 → dom 𝐹 ≈ 𝐹) |