Step | Hyp | Ref
| Expression |
1 | | f1f 5035 |
. . 3
⊢ (𝐹:A–1-1→B →
𝐹:A⟶B) |
2 | | fo2ndf 5790 |
. . 3
⊢ (𝐹:A⟶B
→ (2nd ↾ 𝐹):𝐹–onto→ran 𝐹) |
3 | 1, 2 | syl 14 |
. 2
⊢ (𝐹:A–1-1→B →
(2nd ↾ 𝐹):𝐹–onto→ran 𝐹) |
4 | | f2ndf 5789 |
. . . . 5
⊢ (𝐹:A⟶B
→ (2nd ↾ 𝐹):𝐹⟶B) |
5 | 1, 4 | syl 14 |
. . . 4
⊢ (𝐹:A–1-1→B →
(2nd ↾ 𝐹):𝐹⟶B) |
6 | | fssxp 5001 |
. . . . . . 7
⊢ (𝐹:A⟶B
→ 𝐹 ⊆ (A × B)) |
7 | 1, 6 | syl 14 |
. . . . . 6
⊢ (𝐹:A–1-1→B →
𝐹 ⊆ (A × B)) |
8 | | ssel2 2934 |
. . . . . . . . . . 11
⊢ ((𝐹 ⊆ (A × B)
∧ x ∈ 𝐹) → x ∈ (A × B)) |
9 | | elxp2 4306 |
. . . . . . . . . . 11
⊢ (x ∈ (A × B)
↔ ∃𝑎 ∈ A ∃v ∈ B x =
〈𝑎, v〉) |
10 | 8, 9 | sylib 127 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (A × B)
∧ x ∈ 𝐹) → ∃𝑎 ∈ A ∃v ∈ B x =
〈𝑎, v〉) |
11 | | ssel2 2934 |
. . . . . . . . . . 11
⊢ ((𝐹 ⊆ (A × B)
∧ y ∈ 𝐹) → y ∈ (A × B)) |
12 | | elxp2 4306 |
. . . . . . . . . . 11
⊢ (y ∈ (A × B)
↔ ∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉) |
13 | 11, 12 | sylib 127 |
. . . . . . . . . 10
⊢ ((𝐹 ⊆ (A × B)
∧ y ∈ 𝐹) → ∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉) |
14 | 10, 13 | anim12dan 532 |
. . . . . . . . 9
⊢ ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (∃𝑎 ∈ A ∃v ∈ B x =
〈𝑎, v〉 ∧ ∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉)) |
15 | | fvres 5141 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(〈𝑎, v〉 ∈ 𝐹 → ((2nd ↾
𝐹)‘〈𝑎, v〉) = (2nd ‘〈𝑎, v〉)) |
16 | 15 | adantr 261 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) → ((2nd ↾ 𝐹)‘〈𝑎, v〉) = (2nd ‘〈𝑎, v〉)) |
17 | 16 | adantr 261 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → ((2nd ↾ 𝐹)‘〈𝑎, v〉) = (2nd ‘〈𝑎, v〉)) |
18 | | fvres 5141 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(〈𝑏, w〉 ∈ 𝐹 → ((2nd ↾
𝐹)‘〈𝑏, w〉) = (2nd ‘〈𝑏, w〉)) |
19 | 18 | ad2antlr 458 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → ((2nd ↾ 𝐹)‘〈𝑏, w〉) = (2nd ‘〈𝑏, w〉)) |
20 | 17, 19 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → (((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) ↔ (2nd ‘〈𝑎, v〉) = (2nd ‘〈𝑏, w〉))) |
21 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑎 ∈ V |
22 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ v ∈
V |
23 | 21, 22 | op2nd 5716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑎, v〉) = v |
24 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 𝑏 ∈ V |
25 | | vex 2554 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ w ∈
V |
26 | 24, 25 | op2nd 5716 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(2nd ‘〈𝑏, w〉) = w |
27 | 23, 26 | eqeq12i 2050 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
((2nd ‘〈𝑎, v〉) = (2nd ‘〈𝑏, w〉) ↔ v = w) |
28 | | f1fun 5037 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹:A–1-1→B →
Fun 𝐹) |
29 | | funopfv 5156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Fun
𝐹 → (〈𝑎, v〉 ∈ 𝐹 → (𝐹‘𝑎) = v)) |
30 | | funopfv 5156 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (Fun
𝐹 → (〈𝑏, w〉 ∈ 𝐹 → (𝐹‘𝑏) = w)) |
31 | 29, 30 | anim12d 318 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (Fun
𝐹 → ((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) → ((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w))) |
32 | 28, 31 | syl 14 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:A–1-1→B →
((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) → ((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w))) |
33 | | eqcom 2039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹‘𝑎) = v
↔ v = (𝐹‘𝑎)) |
34 | 33 | biimpi 113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹‘𝑎) = v
→ v = (𝐹‘𝑎)) |
35 | | eqcom 2039 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹‘𝑏) = w
↔ w = (𝐹‘𝑏)) |
36 | 35 | biimpi 113 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ ((𝐹‘𝑏) = w
→ w = (𝐹‘𝑏)) |
37 | 34, 36 | eqeqan12d 2052 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ (((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (v = w ↔ (𝐹‘𝑎) = (𝐹‘𝑏))) |
38 | | simpl 102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑎 ∈ A ∧ v ∈ B) →
𝑎 ∈ A) |
39 | | simpl 102 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . . 38
⊢ ((𝑏 ∈ A ∧ w ∈ B) →
𝑏 ∈ A) |
40 | 38, 39 | anim12i 321 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (𝑎 ∈ A ∧ 𝑏 ∈ A)) |
41 | | f1veqaeq 5351 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝐹:A–1-1→B ∧ (𝑎 ∈ A ∧ 𝑏 ∈ A)) → ((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
42 | 40, 41 | sylan2 270 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ ((𝐹:A–1-1→B ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) →
((𝐹‘𝑎) = (𝐹‘𝑏) → 𝑎 = 𝑏)) |
43 | | opeq12 3542 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . . 37
⊢ ((𝑎 = 𝑏 ∧ v = w) →
〈𝑎, v〉 = 〈𝑏, w〉) |
44 | 43 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. . 36
⊢ (𝑎 = 𝑏 → (v = w →
〈𝑎, v〉 = 〈𝑏, w〉)) |
45 | 42, 44 | syl6 29 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
. 35
⊢ ((𝐹:A–1-1→B ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) →
((𝐹‘𝑎) = (𝐹‘𝑏) → (v = w →
〈𝑎, v〉 = 〈𝑏, w〉))) |
46 | 45 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
34
⊢ ((𝐹:A–1-1→B ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) →
(v = w
→ ((𝐹‘𝑎) = (𝐹‘𝑏) → 〈𝑎, v〉
= 〈𝑏, w〉))) |
47 | 46 | ex 108 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
33
⊢ (𝐹:A–1-1→B →
(((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (v =
w → ((𝐹‘𝑎) = (𝐹‘𝑏) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
48 | 47 | com14 82 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
32
⊢ ((𝐹‘𝑎) = (𝐹‘𝑏) → (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(v = w
→ (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉)))) |
49 | 37, 48 | syl6bi 152 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . . .
31
⊢ (((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (v = w → (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(v = w
→ (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉))))) |
50 | 49 | com14 82 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . .
30
⊢ (v = w →
(v = w
→ (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉))))) |
51 | 50 | pm2.43i 43 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
⊢ (v = w →
(((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉)))) |
52 | 51 | com14 82 |
. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
⊢ (𝐹:A–1-1→B →
(((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (v = w → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
53 | 52 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . . . . . 27
⊢ (𝐹:A–1-1→B →
(((𝐹‘𝑎) = v
∧ (𝐹‘𝑏) = w)
→ (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → (v =
w → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
54 | 32, 53 | syld 40 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝐹:A–1-1→B →
((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) → (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(v = w
→ 〈𝑎, v〉 = 〈𝑏, w〉)))) |
55 | 54 | com13 74 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → ((〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹) → (𝐹:A–1-1→B →
(v = w
→ 〈𝑎, v〉 = 〈𝑏, w〉)))) |
56 | 55 | impcom 116 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → (𝐹:A–1-1→B →
(v = w
→ 〈𝑎, v〉 = 〈𝑏, w〉))) |
57 | 56 | com23 72 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → (v =
w → (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉))) |
58 | 27, 57 | syl5bi 141 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → ((2nd ‘〈𝑎, v〉) = (2nd ‘〈𝑏, w〉) → (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉))) |
59 | 20, 58 | sylbid 139 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → (((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → (𝐹:A–1-1→B →
〈𝑎, v〉 = 〈𝑏, w〉))) |
60 | 59 | com23 72 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) ∧ ((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B))) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉))) |
61 | 60 | ex 108 |
. . . . . . . . . . . . . . . . . . 19
⊢
((〈𝑎, v〉 ∈ 𝐹 ∧ 〈𝑏, w〉
∈ 𝐹) → (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
62 | 61 | adantl 262 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐹 ⊆ (A × B)
∧ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹)) → (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
63 | 62 | com12 27 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑎 ∈ A ∧ v ∈ B) ∧ (𝑏 ∈ A ∧ w ∈ B)) → ((𝐹 ⊆ (A × B)
∧ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
64 | 63 | adantlr 446 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
((𝐹 ⊆ (A × B)
∧ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
65 | 64 | adantr 261 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((𝐹 ⊆ (A × B)
∧ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
66 | | eleq1 2097 |
. . . . . . . . . . . . . . . . . 18
⊢ (x = 〈𝑎, v〉
→ (x ∈ 𝐹 ↔ 〈𝑎, v〉
∈ 𝐹)) |
67 | 66 | ad2antlr 458 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(x ∈
𝐹 ↔ 〈𝑎, v〉 ∈ 𝐹)) |
68 | | eleq1 2097 |
. . . . . . . . . . . . . . . . 17
⊢ (y = 〈𝑏, w〉
→ (y ∈ 𝐹 ↔ 〈𝑏, w〉
∈ 𝐹)) |
69 | 67, 68 | bi2anan9 538 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((x ∈ 𝐹 ∧ y ∈ 𝐹) ↔ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹))) |
70 | 69 | anbi2d 437 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) ↔ (𝐹 ⊆ (A × B)
∧ (〈𝑎, v〉
∈ 𝐹 ∧
〈𝑏, w〉 ∈ 𝐹)))) |
71 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . . 19
⊢ (x = 〈𝑎, v〉
→ ((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘〈𝑎, v〉)) |
72 | 71 | ad2antlr 458 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘〈𝑎, v〉)) |
73 | | fveq2 5121 |
. . . . . . . . . . . . . . . . . 18
⊢ (y = 〈𝑏, w〉
→ ((2nd ↾ 𝐹)‘y) = ((2nd ↾ 𝐹)‘〈𝑏, w〉)) |
74 | 72, 73 | eqeqan12d 2052 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → (((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) ↔ ((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉))) |
75 | | simpllr 486 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → x = 〈𝑎, v〉) |
76 | | simpr 103 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → y = 〈𝑏, w〉) |
77 | 75, 76 | eqeq12d 2051 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → (x = y ↔
〈𝑎, v〉 = 〈𝑏, w〉)) |
78 | 74, 77 | imbi12d 223 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y) ↔ (((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉))) |
79 | 78 | imbi2d 219 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)) ↔ (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘〈𝑎, v〉) = ((2nd ↾ 𝐹)‘〈𝑏, w〉) → 〈𝑎, v〉
= 〈𝑏, w〉)))) |
80 | 65, 70, 79 | 3imtr4d 192 |
. . . . . . . . . . . . . 14
⊢
(((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) ∧ y =
〈𝑏, w〉) → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)))) |
81 | 80 | ex 108 |
. . . . . . . . . . . . 13
⊢ ((((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) ∧ (𝑏 ∈ A ∧ w ∈ B)) →
(y = 〈𝑏, w〉
→ ((𝐹 ⊆
(A × B) ∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))))) |
82 | 81 | rexlimdvva 2434 |
. . . . . . . . . . . 12
⊢ (((𝑎 ∈ A ∧ v ∈ B) ∧ x =
〈𝑎, v〉) → (∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉 → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))))) |
83 | 82 | ex 108 |
. . . . . . . . . . 11
⊢ ((𝑎 ∈ A ∧ v ∈ B) →
(x = 〈𝑎, v〉
→ (∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉 → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)))))) |
84 | 83 | rexlimivv 2432 |
. . . . . . . . . 10
⊢ (∃𝑎 ∈ A ∃v ∈ B x =
〈𝑎, v〉 → (∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉 → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))))) |
85 | 84 | imp 115 |
. . . . . . . . 9
⊢ ((∃𝑎 ∈ A ∃v ∈ B x =
〈𝑎, v〉 ∧ ∃𝑏 ∈ A ∃w ∈ B y =
〈𝑏, w〉) → ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)))) |
86 | 14, 85 | mpcom 32 |
. . . . . . . 8
⊢ ((𝐹 ⊆ (A × B)
∧ (x ∈ 𝐹 ∧ y ∈ 𝐹)) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))) |
87 | 86 | ex 108 |
. . . . . . 7
⊢ (𝐹 ⊆ (A × B)
→ ((x ∈ 𝐹 ∧ y ∈ 𝐹) → (𝐹:A–1-1→B →
(((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)))) |
88 | 87 | com23 72 |
. . . . . 6
⊢ (𝐹 ⊆ (A × B)
→ (𝐹:A–1-1→B →
((x ∈
𝐹 ∧ y ∈ 𝐹) → (((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)))) |
89 | 7, 88 | mpcom 32 |
. . . . 5
⊢ (𝐹:A–1-1→B →
((x ∈
𝐹 ∧ y ∈ 𝐹) → (((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))) |
90 | 89 | ralrimivv 2394 |
. . . 4
⊢ (𝐹:A–1-1→B →
∀x
∈ 𝐹 ∀y ∈ 𝐹 (((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y)) |
91 | | dff13 5350 |
. . . 4
⊢
((2nd ↾ 𝐹):𝐹–1-1→B ↔
((2nd ↾ 𝐹):𝐹⟶B ∧ ∀x ∈ 𝐹 ∀y ∈ 𝐹 (((2nd ↾ 𝐹)‘x) = ((2nd ↾ 𝐹)‘y) → x =
y))) |
92 | 5, 90, 91 | sylanbrc 394 |
. . 3
⊢ (𝐹:A–1-1→B →
(2nd ↾ 𝐹):𝐹–1-1→B) |
93 | | df-f1 4850 |
. . . 4
⊢
((2nd ↾ 𝐹):𝐹–1-1→B ↔
((2nd ↾ 𝐹):𝐹⟶B ∧ Fun ◡(2nd ↾ 𝐹))) |
94 | 93 | simprbi 260 |
. . 3
⊢
((2nd ↾ 𝐹):𝐹–1-1→B →
Fun ◡(2nd ↾ 𝐹)) |
95 | 92, 94 | syl 14 |
. 2
⊢ (𝐹:A–1-1→B →
Fun ◡(2nd ↾ 𝐹)) |
96 | | dff1o3 5075 |
. 2
⊢
((2nd ↾ 𝐹):𝐹–1-1-onto→ran
𝐹 ↔ ((2nd
↾ 𝐹):𝐹–onto→ran 𝐹 ∧ Fun
◡(2nd ↾ 𝐹))) |
97 | 3, 95, 96 | sylanbrc 394 |
1
⊢ (𝐹:A–1-1→B →
(2nd ↾ 𝐹):𝐹–1-1-onto→ran
𝐹) |