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 )