Metamath Proof Explorer


Theorem dmtpos

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

Ref Expression
Assertion dmtpos Rel dom F dom tpos F = dom F -1

Proof

Step Hyp Ref Expression
1 0nelxp ¬ V × V
2 ssel dom F V × V dom F V × V
3 1 2 mtoi dom F V × V ¬ dom F
4 df-rel Rel dom F dom F V × V
5 reldmtpos Rel dom tpos F ¬ dom F
6 3 4 5 3imtr4i Rel dom F Rel dom tpos F
7 relcnv Rel dom F -1
8 6 7 jctir Rel dom F Rel dom tpos F Rel dom F -1
9 vex z V
10 brtpos z V x y tpos F z y x F z
11 9 10 mp1i Rel dom F x y tpos F z y x F z
12 11 exbidv Rel dom F z x y tpos F z z y x F z
13 opex x y V
14 13 eldm x y dom tpos F z x y tpos F z
15 vex x V
16 vex y V
17 15 16 opelcnv x y dom F -1 y x dom F
18 opex y x V
19 18 eldm y x dom F z y x F z
20 17 19 bitri x y dom F -1 z y x F z
21 12 14 20 3bitr4g Rel dom F x y dom tpos F x y dom F -1
22 21 eqrelrdv2 Rel dom tpos F Rel dom F -1 Rel dom F dom tpos F = dom F -1
23 8 22 mpancom Rel dom F dom tpos F = dom F -1