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 V
2 1 elrn z ran tpos F w w tpos F z
3 vex w V
4 3 1 breldm w tpos F z w dom tpos F
5 dmtpos Rel dom F dom tpos F = dom F -1
6 5 eleq2d Rel dom F w dom tpos F w dom F -1
7 4 6 syl5ib Rel dom F w tpos F z w dom F -1
8 relcnv Rel dom F -1
9 elrel Rel dom F -1 w dom F -1 x y w = x y
10 8 9 mpan w dom F -1 x y w = x y
11 7 10 syl6 Rel dom F w tpos F z x y w = x y
12 breq1 w = x y w tpos F z x y tpos F z
13 brtpos z 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 V
17 16 1 brelrn y x F z z ran F
18 15 17 syl6bi w = x y w tpos F z z ran F
19 18 exlimivv x y w = x y w tpos F z z ran F
20 11 19 syli Rel dom F w tpos F z z ran F
21 20 exlimdv Rel dom F w w tpos F z z ran F
22 2 21 syl5bi Rel dom F z ran tpos F z ran F
23 1 elrn z ran F w w F z
24 3 1 breldm w F z w dom F
25 elrel Rel dom F w dom F y x w = y x
26 25 ex Rel dom F w dom F y x w = y x
27 24 26 syl5 Rel dom F w F z y 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 V
31 30 1 brelrn x y tpos F z z ran tpos F
32 29 31 syl6bi w = y x w F z z ran tpos F
33 32 exlimivv y x w = y x w F z z ran tpos F
34 27 33 syli Rel dom F w F z z ran tpos F
35 34 exlimdv Rel dom F w w F z z ran tpos F
36 23 35 syl5bi Rel dom F z ran F z ran tpos F
37 22 36 impbid Rel dom F z ran tpos F z ran F
38 37 eqrdv Rel dom F ran tpos F = ran F