Step | Hyp | Ref
| Expression |
1 | | fndm 5182 |
. . . . . 6
⊢ (F Fn A →
dom F = A) |
2 | | opeldm 4910 |
. . . . . . 7
⊢ (〈z, w〉 ∈ F →
z ∈ dom
F) |
3 | | eleq2 2414 |
. . . . . . 7
⊢ (dom F = A →
(z ∈ dom
F ↔ z ∈ A)) |
4 | 2, 3 | syl5ib 210 |
. . . . . 6
⊢ (dom F = A →
(〈z,
w〉 ∈ F →
z ∈
A)) |
5 | 1, 4 | syl 15 |
. . . . 5
⊢ (F Fn A →
(〈z,
w〉 ∈ F →
z ∈
A)) |
6 | | eleq1 2413 |
. . . . . . . . 9
⊢ (x = z →
(x ∈
A ↔ z ∈ A)) |
7 | 6 | biimpcd 215 |
. . . . . . . 8
⊢ (x ∈ A → (x =
z → z ∈ A)) |
8 | 7 | adantrd 454 |
. . . . . . 7
⊢ (x ∈ A → ((x =
z ∧
(F ‘x) = w) →
z ∈
A)) |
9 | 8 | rexlimiv 2732 |
. . . . . 6
⊢ (∃x ∈ A (x = z ∧ (F
‘x) = w) → z
∈ A) |
10 | 9 | a1i 10 |
. . . . 5
⊢ (F Fn A →
(∃x
∈ A
(x = z
∧ (F
‘x) = w) → z
∈ A)) |
11 | | fveq2 5328 |
. . . . . . . . . 10
⊢ (x = z →
(F ‘x) = (F
‘z)) |
12 | 11 | eqeq1d 2361 |
. . . . . . . . 9
⊢ (x = z →
((F ‘x) = w ↔
(F ‘z) = w)) |
13 | 12 | ceqsrexv 2972 |
. . . . . . . 8
⊢ (z ∈ A → (∃x ∈ A (x = z ∧ (F
‘x) = w) ↔ (F
‘z) = w)) |
14 | 13 | adantl 452 |
. . . . . . 7
⊢ ((F Fn A ∧ z ∈ A) →
(∃x
∈ A
(x = z
∧ (F
‘x) = w) ↔ (F
‘z) = w)) |
15 | | fnopfvb 5359 |
. . . . . . 7
⊢ ((F Fn A ∧ z ∈ A) →
((F ‘z) = w ↔
〈z,
w〉 ∈ F)) |
16 | 14, 15 | bitr2d 245 |
. . . . . 6
⊢ ((F Fn A ∧ z ∈ A) →
(〈z,
w〉 ∈ F ↔
∃x ∈ A (x = z ∧ (F
‘x) = w))) |
17 | 16 | ex 423 |
. . . . 5
⊢ (F Fn A →
(z ∈
A → (〈z, w〉 ∈ F ↔
∃x ∈ A (x = z ∧ (F
‘x) = w)))) |
18 | 5, 10, 17 | pm5.21ndd 343 |
. . . 4
⊢ (F Fn A →
(〈z,
w〉 ∈ F ↔
∃x ∈ A (x = z ∧ (F
‘x) = w))) |
19 | | vex 2862 |
. . . . . 6
⊢ z ∈
V |
20 | | vex 2862 |
. . . . . 6
⊢ w ∈
V |
21 | 19, 20 | opex 4588 |
. . . . 5
⊢ 〈z, w〉 ∈ V |
22 | | eqeq1 2359 |
. . . . . . 7
⊢ (y = 〈z, w〉 → (y =
〈x,
(F ‘x)〉 ↔ 〈z, w〉 = 〈x, (F ‘x)〉)) |
23 | | eqcom 2355 |
. . . . . . . 8
⊢ (〈z, w〉 = 〈x, (F ‘x)〉 ↔ 〈x, (F ‘x)〉 = 〈z, w〉) |
24 | | opth 4602 |
. . . . . . . 8
⊢ (〈x, (F ‘x)〉 = 〈z, w〉 ↔ (x =
z ∧
(F ‘x) = w)) |
25 | 23, 24 | bitri 240 |
. . . . . . 7
⊢ (〈z, w〉 = 〈x, (F ‘x)〉 ↔ (x =
z ∧
(F ‘x) = w)) |
26 | 22, 25 | syl6bb 252 |
. . . . . 6
⊢ (y = 〈z, w〉 → (y =
〈x,
(F ‘x)〉 ↔
(x = z
∧ (F
‘x) = w))) |
27 | 26 | rexbidv 2635 |
. . . . 5
⊢ (y = 〈z, w〉 → (∃x ∈ A y = 〈x, (F
‘x)〉 ↔ ∃x ∈ A (x = z ∧ (F
‘x) = w))) |
28 | 21, 27 | elab 2985 |
. . . 4
⊢ (〈z, w〉 ∈ {y ∣ ∃x ∈ A y = 〈x, (F ‘x)〉} ↔ ∃x ∈ A (x = z ∧ (F
‘x) = w)) |
29 | 18, 28 | syl6bbr 254 |
. . 3
⊢ (F Fn A →
(〈z,
w〉 ∈ F ↔
〈z,
w〉 ∈ {y ∣ ∃x ∈ A y = 〈x, (F ‘x)〉})) |
30 | 29 | eqrelrdv 4852 |
. 2
⊢ (F Fn A →
F = {y
∣ ∃x ∈ A y = 〈x, (F
‘x)〉}) |
31 | | rnopab2 4968 |
. 2
⊢ ran {〈x, y〉 ∣ (x ∈ A ∧ y = 〈x, (F ‘x)〉)} = {y ∣ ∃x ∈ A y = 〈x, (F ‘x)〉} |
32 | 30, 31 | syl6eqr 2403 |
1
⊢ (F Fn A →
F = ran {〈x, y〉 ∣ (x ∈ A ∧ y = 〈x, (F ‘x)〉)}) |