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 )