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 <-> -. (/) e. dom F )

Proof

Step Hyp Ref Expression
1 0ex 
 |-  (/) e. _V
2 1 eldm 
 |-  ( (/) e. dom F <-> E. y (/) F y )
3 brtpos0 
 |-  ( y e. _V -> ( (/) tpos F y <-> (/) F y ) )
4 3 elv 
 |-  ( (/) tpos F y <-> (/) F y )
5 0nelrel0 
 |-  ( Rel dom tpos F -> -. (/) e. dom tpos F )
6 vex 
 |-  y e. _V
7 1 6 breldm 
 |-  ( (/) tpos F y -> (/) e. 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 
 |-  ( E. y (/) F y -> -. Rel dom tpos F )
11 2 10 sylbi 
 |-  ( (/) e. dom F -> -. Rel dom tpos F )
12 11 con2i 
 |-  ( Rel dom tpos F -> -. (/) e. dom F )
13 vex 
 |-  x e. _V
14 13 eldm 
 |-  ( x e. dom tpos F <-> E. y x tpos F y )
15 relcnv 
 |-  Rel `' dom F
16 df-rel 
 |-  ( Rel `' dom F <-> `' dom F C_ ( _V X. _V ) )
17 15 16 mpbi 
 |-  `' dom F C_ ( _V X. _V )
18 17 sseli 
 |-  ( x e. `' dom F -> x e. ( _V X. _V ) )
19 18 a1i 
 |-  ( ( -. (/) e. dom F /\ x tpos F y ) -> ( x e. `' dom F -> x e. ( _V X. _V ) ) )
20 elsni 
 |-  ( x e. { (/) } -> x = (/) )
21 20 breq1d 
 |-  ( x e. { (/) } -> ( x tpos F y <-> (/) tpos F y ) )
22 1 6 breldm 
 |-  ( (/) F y -> (/) e. dom F )
23 22 pm2.24d 
 |-  ( (/) F y -> ( -. (/) e. dom F -> x e. ( _V X. _V ) ) )
24 4 23 sylbi 
 |-  ( (/) tpos F y -> ( -. (/) e. dom F -> x e. ( _V X. _V ) ) )
25 21 24 syl6bi 
 |-  ( x e. { (/) } -> ( x tpos F y -> ( -. (/) e. dom F -> x e. ( _V X. _V ) ) ) )
26 25 com3l 
 |-  ( x tpos F y -> ( -. (/) e. dom F -> ( x e. { (/) } -> x e. ( _V X. _V ) ) ) )
27 26 impcom 
 |-  ( ( -. (/) e. dom F /\ x tpos F y ) -> ( x e. { (/) } -> x e. ( _V X. _V ) ) )
28 brtpos2 
 |-  ( y e. _V -> ( x tpos F y <-> ( x e. ( `' dom F u. { (/) } ) /\ U. `' { x } F y ) ) )
29 6 28 ax-mp 
 |-  ( x tpos F y <-> ( x e. ( `' dom F u. { (/) } ) /\ U. `' { x } F y ) )
30 29 simplbi 
 |-  ( x tpos F y -> x e. ( `' dom F u. { (/) } ) )
31 elun 
 |-  ( x e. ( `' dom F u. { (/) } ) <-> ( x e. `' dom F \/ x e. { (/) } ) )
32 30 31 sylib 
 |-  ( x tpos F y -> ( x e. `' dom F \/ x e. { (/) } ) )
33 32 adantl 
 |-  ( ( -. (/) e. dom F /\ x tpos F y ) -> ( x e. `' dom F \/ x e. { (/) } ) )
34 19 27 33 mpjaod 
 |-  ( ( -. (/) e. dom F /\ x tpos F y ) -> x e. ( _V X. _V ) )
35 34 ex 
 |-  ( -. (/) e. dom F -> ( x tpos F y -> x e. ( _V X. _V ) ) )
36 35 exlimdv 
 |-  ( -. (/) e. dom F -> ( E. y x tpos F y -> x e. ( _V X. _V ) ) )
37 14 36 syl5bi 
 |-  ( -. (/) e. dom F -> ( x e. dom tpos F -> x e. ( _V X. _V ) ) )
38 37 ssrdv 
 |-  ( -. (/) e. dom F -> dom tpos F C_ ( _V X. _V ) )
39 df-rel 
 |-  ( Rel dom tpos F <-> dom tpos F C_ ( _V X. _V ) )
40 38 39 sylibr 
 |-  ( -. (/) e. dom F -> Rel dom tpos F )
41 12 40 impbii 
 |-  ( Rel dom tpos F <-> -. (/) e. dom F )