Step | Hyp | Ref
| Expression |
1 | | vex 2554 |
. . . . 5
⊢ x ∈
V |
2 | 1 | elrn 4520 |
. . . 4
⊢ (x ∈ ran tpos 𝐹 ↔ ∃y ytpos 𝐹x) |
3 | | vex 2554 |
. . . . . . . . 9
⊢ y ∈
V |
4 | 3, 1 | breldm 4482 |
. . . . . . . 8
⊢ (ytpos 𝐹x →
y ∈ dom
tpos 𝐹) |
5 | | dmtpos 5812 |
. . . . . . . . 9
⊢ (Rel dom
𝐹 → dom tpos 𝐹 = ◡dom 𝐹) |
6 | 5 | eleq2d 2104 |
. . . . . . . 8
⊢ (Rel dom
𝐹 → (y ∈ dom tpos 𝐹 ↔ y ∈ ◡dom 𝐹)) |
7 | 4, 6 | syl5ib 143 |
. . . . . . 7
⊢ (Rel dom
𝐹 → (ytpos 𝐹x →
y ∈ ◡dom 𝐹)) |
8 | | relcnv 4646 |
. . . . . . . 8
⊢ Rel ◡dom 𝐹 |
9 | | elrel 4385 |
. . . . . . . 8
⊢ ((Rel
◡dom 𝐹 ∧ y ∈ ◡dom 𝐹) → ∃w∃z y = 〈w,
z〉) |
10 | 8, 9 | mpan 400 |
. . . . . . 7
⊢ (y ∈ ◡dom 𝐹 → ∃w∃z y = 〈w,
z〉) |
11 | 7, 10 | syl6 29 |
. . . . . 6
⊢ (Rel dom
𝐹 → (ytpos 𝐹x →
∃w∃z y = 〈w,
z〉)) |
12 | | breq1 3758 |
. . . . . . . . 9
⊢ (y = 〈w,
z〉 → (ytpos 𝐹x ↔
〈w, z〉tpos 𝐹x)) |
13 | | vex 2554 |
. . . . . . . . . 10
⊢ w ∈
V |
14 | | vex 2554 |
. . . . . . . . . 10
⊢ z ∈
V |
15 | | brtposg 5810 |
. . . . . . . . . 10
⊢
((w ∈ V ∧ z ∈ V ∧ x ∈ V) → (〈w, z〉tpos
𝐹x ↔ 〈z, w〉𝐹x)) |
16 | 13, 14, 1, 15 | mp3an 1231 |
. . . . . . . . 9
⊢
(〈w, z〉tpos 𝐹x ↔
〈z, w〉𝐹x) |
17 | 12, 16 | syl6bb 185 |
. . . . . . . 8
⊢ (y = 〈w,
z〉 → (ytpos 𝐹x ↔
〈z, w〉𝐹x)) |
18 | 14, 13 | opex 3957 |
. . . . . . . . 9
⊢
〈z, w〉 ∈
V |
19 | 18, 1 | brelrn 4510 |
. . . . . . . 8
⊢
(〈z, w〉𝐹x →
x ∈ ran
𝐹) |
20 | 17, 19 | syl6bi 152 |
. . . . . . 7
⊢ (y = 〈w,
z〉 → (ytpos 𝐹x →
x ∈ ran
𝐹)) |
21 | 20 | exlimivv 1773 |
. . . . . 6
⊢ (∃w∃z y = 〈w,
z〉 → (ytpos 𝐹x →
x ∈ ran
𝐹)) |
22 | 11, 21 | syli 33 |
. . . . 5
⊢ (Rel dom
𝐹 → (ytpos 𝐹x →
x ∈ ran
𝐹)) |
23 | 22 | exlimdv 1697 |
. . . 4
⊢ (Rel dom
𝐹 → (∃y ytpos 𝐹x →
x ∈ ran
𝐹)) |
24 | 2, 23 | syl5bi 141 |
. . 3
⊢ (Rel dom
𝐹 → (x ∈ ran tpos 𝐹 → x ∈ ran 𝐹)) |
25 | 1 | elrn 4520 |
. . . 4
⊢ (x ∈ ran 𝐹 ↔ ∃y y𝐹x) |
26 | 3, 1 | breldm 4482 |
. . . . . . 7
⊢ (y𝐹x →
y ∈ dom
𝐹) |
27 | | elrel 4385 |
. . . . . . . 8
⊢ ((Rel dom
𝐹 ∧ y ∈ dom 𝐹) → ∃z∃w y = 〈z,
w〉) |
28 | 27 | ex 108 |
. . . . . . 7
⊢ (Rel dom
𝐹 → (y ∈ dom 𝐹 → ∃z∃w y = 〈z,
w〉)) |
29 | 26, 28 | syl5 28 |
. . . . . 6
⊢ (Rel dom
𝐹 → (y𝐹x →
∃z∃w y = 〈z,
w〉)) |
30 | | breq1 3758 |
. . . . . . . . 9
⊢ (y = 〈z,
w〉 → (y𝐹x ↔
〈z, w〉𝐹x)) |
31 | 30, 16 | syl6bbr 187 |
. . . . . . . 8
⊢ (y = 〈z,
w〉 → (y𝐹x ↔
〈w, z〉tpos 𝐹x)) |
32 | 13, 14 | opex 3957 |
. . . . . . . . 9
⊢
〈w, z〉 ∈
V |
33 | 32, 1 | brelrn 4510 |
. . . . . . . 8
⊢
(〈w, z〉tpos 𝐹x →
x ∈ ran
tpos 𝐹) |
34 | 31, 33 | syl6bi 152 |
. . . . . . 7
⊢ (y = 〈z,
w〉 → (y𝐹x →
x ∈ ran
tpos 𝐹)) |
35 | 34 | exlimivv 1773 |
. . . . . 6
⊢ (∃z∃w y = 〈z,
w〉 → (y𝐹x →
x ∈ ran
tpos 𝐹)) |
36 | 29, 35 | syli 33 |
. . . . 5
⊢ (Rel dom
𝐹 → (y𝐹x →
x ∈ ran
tpos 𝐹)) |
37 | 36 | exlimdv 1697 |
. . . 4
⊢ (Rel dom
𝐹 → (∃y y𝐹x →
x ∈ ran
tpos 𝐹)) |
38 | 25, 37 | syl5bi 141 |
. . 3
⊢ (Rel dom
𝐹 → (x ∈ ran 𝐹 → x ∈ ran tpos 𝐹)) |
39 | 24, 38 | impbid 120 |
. 2
⊢ (Rel dom
𝐹 → (x ∈ ran tpos 𝐹 ↔ x ∈ ran 𝐹)) |
40 | 39 | eqrdv 2035 |
1
⊢ (Rel dom
𝐹 → ran tpos 𝐹 = ran 𝐹) |