Step | Hyp | Ref
| Expression |
1 | | fundmen.1 |
. . . 4
⊢ 𝐹 ∈ V |
2 | 1 | dmex 4598 |
. . 3
⊢ dom 𝐹 ∈ V |
3 | 2 | a1i 9 |
. 2
⊢ (Fun
𝐹 → dom 𝐹 ∈ V) |
4 | 1 | a1i 9 |
. 2
⊢ (Fun
𝐹 → 𝐹 ∈ V) |
5 | | funfvop 5279 |
. . 3
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹) |
6 | 5 | ex 108 |
. 2
⊢ (Fun
𝐹 → (𝑥 ∈ dom 𝐹 → 〈𝑥, (𝐹‘𝑥)〉 ∈ 𝐹)) |
7 | | funrel 4919 |
. . 3
⊢ (Fun
𝐹 → Rel 𝐹) |
8 | | elreldm 4560 |
. . . 4
⊢ ((Rel
𝐹 ∧ 𝑦 ∈ 𝐹) → ∩ ∩ 𝑦
∈ dom 𝐹) |
9 | 8 | ex 108 |
. . 3
⊢ (Rel
𝐹 → (𝑦 ∈ 𝐹 → ∩ ∩ 𝑦
∈ dom 𝐹)) |
10 | 7, 9 | syl 14 |
. 2
⊢ (Fun
𝐹 → (𝑦 ∈ 𝐹 → ∩ ∩ 𝑦
∈ dom 𝐹)) |
11 | | df-rel 4352 |
. . . . . . . . 9
⊢ (Rel
𝐹 ↔ 𝐹 ⊆ (V × V)) |
12 | 7, 11 | sylib 127 |
. . . . . . . 8
⊢ (Fun
𝐹 → 𝐹 ⊆ (V × V)) |
13 | 12 | sselda 2945 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → 𝑦 ∈ (V × V)) |
14 | | elvv 4402 |
. . . . . . 7
⊢ (𝑦 ∈ (V × V) ↔
∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉) |
15 | 13, 14 | sylib 127 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → ∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉) |
16 | | inteq 3618 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
𝑦 = ∩ 〈𝑧, 𝑤〉) |
17 | 16 | inteqd 3620 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑧, 𝑤〉) |
18 | | vex 2560 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑧 ∈ V |
19 | | vex 2560 |
. . . . . . . . . . . . . . . . 17
⊢ 𝑤 ∈ V |
20 | 18, 19 | op1stb 4209 |
. . . . . . . . . . . . . . . 16
⊢ ∩ ∩ 〈𝑧, 𝑤〉 = 𝑧 |
21 | 17, 20 | syl6eq 2088 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = 〈𝑧, 𝑤〉 → ∩
∩ 𝑦 = 𝑧) |
22 | | eqeq1 2046 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑥 = 𝑧 ↔ ∩ ∩ 𝑦 =
𝑧)) |
23 | 21, 22 | syl5ibr 145 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → 𝑥 = 𝑧)) |
24 | | opeq1 3549 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) |
25 | 23, 24 | syl6 29 |
. . . . . . . . . . . . 13
⊢ (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉)) |
26 | 25 | imp 115 |
. . . . . . . . . . . 12
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → 〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉) |
27 | | eqeq2 2049 |
. . . . . . . . . . . . . 14
⊢
(〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → (𝑦 = 〈𝑥, 𝑤〉 ↔ 𝑦 = 〈𝑧, 𝑤〉)) |
28 | 27 | biimprcd 149 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 〈𝑧, 𝑤〉 → (〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → 𝑦 = 〈𝑥, 𝑤〉)) |
29 | 28 | adantl 262 |
. . . . . . . . . . . 12
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → (〈𝑥, 𝑤〉 = 〈𝑧, 𝑤〉 → 𝑦 = 〈𝑥, 𝑤〉)) |
30 | 26, 29 | mpd 13 |
. . . . . . . . . . 11
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → 𝑦 = 〈𝑥, 𝑤〉) |
31 | 30 | ancoms 255 |
. . . . . . . . . 10
⊢ ((𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦)
→ 𝑦 = 〈𝑥, 𝑤〉) |
32 | 31 | adantl 262 |
. . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 𝑦 = 〈𝑥, 𝑤〉) |
33 | 30 | eleq1d 2106 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 = ∩
∩ 𝑦 ∧ 𝑦 = 〈𝑧, 𝑤〉) → (𝑦 ∈ 𝐹 ↔ 〈𝑥, 𝑤〉 ∈ 𝐹)) |
34 | 33 | adantl 262 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (𝑦 ∈ 𝐹 ↔ 〈𝑥, 𝑤〉 ∈ 𝐹)) |
35 | | funopfv 5213 |
. . . . . . . . . . . . . . 15
⊢ (Fun
𝐹 → (〈𝑥, 𝑤〉 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) |
36 | 35 | adantr 261 |
. . . . . . . . . . . . . 14
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (〈𝑥, 𝑤〉 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) |
37 | 34, 36 | sylbid 139 |
. . . . . . . . . . . . 13
⊢ ((Fun
𝐹 ∧ (𝑥 = ∩ ∩ 𝑦
∧ 𝑦 = 〈𝑧, 𝑤〉)) → (𝑦 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)) |
38 | 37 | exp32 347 |
. . . . . . . . . . . 12
⊢ (Fun
𝐹 → (𝑥 = ∩
∩ 𝑦 → (𝑦 = 〈𝑧, 𝑤〉 → (𝑦 ∈ 𝐹 → (𝐹‘𝑥) = 𝑤)))) |
39 | 38 | com24 81 |
. . . . . . . . . . 11
⊢ (Fun
𝐹 → (𝑦 ∈ 𝐹 → (𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ (𝐹‘𝑥) = 𝑤)))) |
40 | 39 | imp43 337 |
. . . . . . . . . 10
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ (𝐹‘𝑥) = 𝑤) |
41 | 40 | opeq2d 3556 |
. . . . . . . . 9
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 〈𝑥, (𝐹‘𝑥)〉 = 〈𝑥, 𝑤〉) |
42 | 32, 41 | eqtr4d 2075 |
. . . . . . . 8
⊢ (((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) ∧ (𝑦 = 〈𝑧, 𝑤〉 ∧ 𝑥 = ∩ ∩ 𝑦))
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉) |
43 | 42 | exp32 347 |
. . . . . . 7
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) |
44 | 43 | exlimdvv 1777 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (∃𝑧∃𝑤 𝑦 = 〈𝑧, 𝑤〉 → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) |
45 | 15, 44 | mpd 13 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) |
46 | 45 | adantrl 447 |
. . . 4
⊢ ((Fun
𝐹 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 = ∩ ∩ 𝑦
→ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) |
47 | | inteq 3618 |
. . . . . . . . 9
⊢ (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → ∩
𝑦 = ∩ 〈𝑥, (𝐹‘𝑥)〉) |
48 | 47 | inteqd 3620 |
. . . . . . . 8
⊢ (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉) |
49 | 48 | adantl 262 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉) → ∩
∩ 𝑦 = ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉) |
50 | | vex 2560 |
. . . . . . . . 9
⊢ 𝑥 ∈ V |
51 | | funfvex 5192 |
. . . . . . . . 9
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝐹‘𝑥) ∈ V) |
52 | | op1stbg 4210 |
. . . . . . . . 9
⊢ ((𝑥 ∈ V ∧ (𝐹‘𝑥) ∈ V) → ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉 = 𝑥) |
53 | 50, 51, 52 | sylancr 393 |
. . . . . . . 8
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → ∩ ∩ 〈𝑥, (𝐹‘𝑥)〉 = 𝑥) |
54 | 53 | adantr 261 |
. . . . . . 7
⊢ (((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉) → ∩
∩ 〈𝑥, (𝐹‘𝑥)〉 = 𝑥) |
55 | 49, 54 | eqtr2d 2073 |
. . . . . 6
⊢ (((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) ∧ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉) → 𝑥 = ∩ ∩ 𝑦) |
56 | 55 | ex 108 |
. . . . 5
⊢ ((Fun
𝐹 ∧ 𝑥 ∈ dom 𝐹) → (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → 𝑥 = ∩ ∩ 𝑦)) |
57 | 56 | adantrr 448 |
. . . 4
⊢ ((Fun
𝐹 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑦 = 〈𝑥, (𝐹‘𝑥)〉 → 𝑥 = ∩ ∩ 𝑦)) |
58 | 46, 57 | impbid 120 |
. . 3
⊢ ((Fun
𝐹 ∧ (𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹)) → (𝑥 = ∩ ∩ 𝑦
↔ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉)) |
59 | 58 | ex 108 |
. 2
⊢ (Fun
𝐹 → ((𝑥 ∈ dom 𝐹 ∧ 𝑦 ∈ 𝐹) → (𝑥 = ∩ ∩ 𝑦
↔ 𝑦 = 〈𝑥, (𝐹‘𝑥)〉))) |
60 | 3, 4, 6, 10, 59 | en3d 6249 |
1
⊢ (Fun
𝐹 → dom 𝐹 ≈ 𝐹) |