Step |
Hyp |
Ref |
Expression |
1 |
|
vex |
|- z e. _V |
2 |
1
|
elrn |
|- ( z e. ran tpos F <-> E. w w tpos F z ) |
3 |
|
vex |
|- w e. _V |
4 |
3 1
|
breldm |
|- ( w tpos F z -> w e. dom tpos F ) |
5 |
|
dmtpos |
|- ( Rel dom F -> dom tpos F = `' dom F ) |
6 |
5
|
eleq2d |
|- ( Rel dom F -> ( w e. dom tpos F <-> w e. `' dom F ) ) |
7 |
4 6
|
syl5ib |
|- ( Rel dom F -> ( w tpos F z -> w e. `' dom F ) ) |
8 |
|
relcnv |
|- Rel `' dom F |
9 |
|
elrel |
|- ( ( Rel `' dom F /\ w e. `' dom F ) -> E. x E. y w = <. x , y >. ) |
10 |
8 9
|
mpan |
|- ( w e. `' dom F -> E. x E. y w = <. x , y >. ) |
11 |
7 10
|
syl6 |
|- ( Rel dom F -> ( w tpos F z -> E. x E. y w = <. x , y >. ) ) |
12 |
|
breq1 |
|- ( w = <. x , y >. -> ( w tpos F z <-> <. x , y >. tpos F z ) ) |
13 |
|
brtpos |
|- ( z e. _V -> ( <. x , y >. tpos F z <-> <. y , x >. F z ) ) |
14 |
13
|
elv |
|- ( <. x , y >. tpos F z <-> <. y , x >. F z ) |
15 |
12 14
|
bitrdi |
|- ( w = <. x , y >. -> ( w tpos F z <-> <. y , x >. F z ) ) |
16 |
|
opex |
|- <. y , x >. e. _V |
17 |
16 1
|
brelrn |
|- ( <. y , x >. F z -> z e. ran F ) |
18 |
15 17
|
syl6bi |
|- ( w = <. x , y >. -> ( w tpos F z -> z e. ran F ) ) |
19 |
18
|
exlimivv |
|- ( E. x E. y w = <. x , y >. -> ( w tpos F z -> z e. ran F ) ) |
20 |
11 19
|
syli |
|- ( Rel dom F -> ( w tpos F z -> z e. ran F ) ) |
21 |
20
|
exlimdv |
|- ( Rel dom F -> ( E. w w tpos F z -> z e. ran F ) ) |
22 |
2 21
|
syl5bi |
|- ( Rel dom F -> ( z e. ran tpos F -> z e. ran F ) ) |
23 |
1
|
elrn |
|- ( z e. ran F <-> E. w w F z ) |
24 |
3 1
|
breldm |
|- ( w F z -> w e. dom F ) |
25 |
|
elrel |
|- ( ( Rel dom F /\ w e. dom F ) -> E. y E. x w = <. y , x >. ) |
26 |
25
|
ex |
|- ( Rel dom F -> ( w e. dom F -> E. y E. x w = <. y , x >. ) ) |
27 |
24 26
|
syl5 |
|- ( Rel dom F -> ( w F z -> E. y E. x w = <. y , x >. ) ) |
28 |
|
breq1 |
|- ( w = <. y , x >. -> ( w F z <-> <. y , x >. F z ) ) |
29 |
28 14
|
bitr4di |
|- ( w = <. y , x >. -> ( w F z <-> <. x , y >. tpos F z ) ) |
30 |
|
opex |
|- <. x , y >. e. _V |
31 |
30 1
|
brelrn |
|- ( <. x , y >. tpos F z -> z e. ran tpos F ) |
32 |
29 31
|
syl6bi |
|- ( w = <. y , x >. -> ( w F z -> z e. ran tpos F ) ) |
33 |
32
|
exlimivv |
|- ( E. y E. x w = <. y , x >. -> ( w F z -> z e. ran tpos F ) ) |
34 |
27 33
|
syli |
|- ( Rel dom F -> ( w F z -> z e. ran tpos F ) ) |
35 |
34
|
exlimdv |
|- ( Rel dom F -> ( E. w w F z -> z e. ran tpos F ) ) |
36 |
23 35
|
syl5bi |
|- ( Rel dom F -> ( z e. ran F -> z e. ran tpos F ) ) |
37 |
22 36
|
impbid |
|- ( Rel dom F -> ( z e. ran tpos F <-> z e. ran F ) ) |
38 |
37
|
eqrdv |
|- ( Rel dom F -> ran tpos F = ran F ) |