This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
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 ) |
| 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 | biimtrdi | |- ( 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 | biimtrid | |- ( -. (/) 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 ) |