Metamath Proof Explorer


Theorem reldmtpos

Description: Necessary and sufficient condition for dom tpos F to be a relation. (Contributed by Mario Carneiro, 10-Sep-2015)

Ref Expression
Assertion reldmtpos Rel dom tpos F ¬ dom F

Proof

Step Hyp Ref Expression
1 0ex V
2 1 eldm dom F y F y
3 brtpos0 y V tpos F y F y
4 3 elv tpos F y F y
5 0nelrel0 Rel dom tpos F ¬ dom tpos F
6 vex y V
7 1 6 breldm tpos F y dom tpos F
8 5 7 nsyl3 tpos F y ¬ Rel dom tpos F
9 4 8 sylbir F y ¬ Rel dom tpos F
10 9 exlimiv y F y ¬ Rel dom tpos F
11 2 10 sylbi dom F ¬ Rel dom tpos F
12 11 con2i Rel dom tpos F ¬ dom F
13 vex x V
14 13 eldm x dom tpos F y x tpos F y
15 relcnv Rel dom F -1
16 df-rel Rel dom F -1 dom F -1 V × V
17 15 16 mpbi dom F -1 V × V
18 17 sseli x dom F -1 x V × V
19 18 a1i ¬ dom F x tpos F y x dom F -1 x V × V
20 elsni x x =
21 20 breq1d x x tpos F y tpos F y
22 1 6 breldm F y dom F
23 22 pm2.24d F y ¬ dom F x V × V
24 4 23 sylbi tpos F y ¬ dom F x V × V
25 21 24 syl6bi x x tpos F y ¬ dom F x V × V
26 25 com3l x tpos F y ¬ dom F x x V × V
27 26 impcom ¬ dom F x tpos F y x x V × V
28 brtpos2 y V x tpos F y x dom F -1 x -1 F y
29 6 28 ax-mp x tpos F y x dom F -1 x -1 F y
30 29 simplbi x tpos F y x dom F -1
31 elun x dom F -1 x dom F -1 x
32 30 31 sylib x tpos F y x dom F -1 x
33 32 adantl ¬ dom F x tpos F y x dom F -1 x
34 19 27 33 mpjaod ¬ dom F x tpos F y x V × V
35 34 ex ¬ dom F x tpos F y x V × V
36 35 exlimdv ¬ dom F y x tpos F y x V × V
37 14 36 syl5bi ¬ dom F x dom tpos F x V × V
38 37 ssrdv ¬ dom F dom tpos F V × V
39 df-rel Rel dom tpos F dom tpos F V × V
40 38 39 sylibr ¬ dom F Rel dom tpos F
41 12 40 impbii Rel dom tpos F ¬ dom F