Metamath Proof Explorer

Theorem rntpos

Description: The range of tpos F when dom F is a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion rntpos 
|- ( Rel dom F -> ran tpos F = ran F )

Proof

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 )