Metamath Proof Explorer

Theorem mpoxopxnop0

Description: If the first argument of an operation given by a maps-to rule, where the first argument is a pair and the base set of the second argument is the first component of the first argument, is not an ordered pair, then the value of the operation is the empty set. (Contributed by Alexander van der Vekens, 10-Oct-2017)

Ref Expression
Hypothesis mpoxopn0yelv.f 
|- F = ( x e. _V , y e. ( 1st ` x ) |-> C )
Assertion mpoxopxnop0 
|- ( -. V e. ( _V X. _V ) -> ( V F K ) = (/) )

Proof

Step Hyp Ref Expression
1 mpoxopn0yelv.f 
 |-  F = ( x e. _V , y e. ( 1st ` x ) |-> C )
2 neq0 
 |-  ( -. ( V F K ) = (/) <-> E. x x e. ( V F K ) )
3 1 dmmpossx 
 |-  dom F C_ U_ x e. _V ( { x } X. ( 1st ` x ) )
4 elfvdm 
 |-  ( x e. ( F ` <. V , K >. ) -> <. V , K >. e. dom F )
5 df-ov 
 |-  ( V F K ) = ( F ` <. V , K >. )
6 4 5 eleq2s 
 |-  ( x e. ( V F K ) -> <. V , K >. e. dom F )
7 3 6 sselid 
 |-  ( x e. ( V F K ) -> <. V , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) )
8 fveq2 
 |-  ( x = V -> ( 1st ` x ) = ( 1st ` V ) )
9 8 opeliunxp2 
 |-  ( <. V , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) <-> ( V e. _V /\ K e. ( 1st ` V ) ) )
10 eluni 
 |-  ( K e. U. dom { V } <-> E. n ( K e. n /\ n e. dom { V } ) )
11 ne0i 
 |-  ( n e. dom { V } -> dom { V } =/= (/) )
12 11 ad2antlr 
 |-  ( ( ( K e. n /\ n e. dom { V } ) /\ V e. _V ) -> dom { V } =/= (/) )
13 dmsnn0 
 |-  ( V e. ( _V X. _V ) <-> dom { V } =/= (/) )
14 12 13 sylibr 
 |-  ( ( ( K e. n /\ n e. dom { V } ) /\ V e. _V ) -> V e. ( _V X. _V ) )
15 14 ex 
 |-  ( ( K e. n /\ n e. dom { V } ) -> ( V e. _V -> V e. ( _V X. _V ) ) )
16 15 exlimiv 
 |-  ( E. n ( K e. n /\ n e. dom { V } ) -> ( V e. _V -> V e. ( _V X. _V ) ) )
17 10 16 sylbi 
 |-  ( K e. U. dom { V } -> ( V e. _V -> V e. ( _V X. _V ) ) )
18 1stval 
 |-  ( 1st ` V ) = U. dom { V }
19 17 18 eleq2s 
 |-  ( K e. ( 1st ` V ) -> ( V e. _V -> V e. ( _V X. _V ) ) )
20 19 impcom 
 |-  ( ( V e. _V /\ K e. ( 1st ` V ) ) -> V e. ( _V X. _V ) )
21 9 20 sylbi 
 |-  ( <. V , K >. e. U_ x e. _V ( { x } X. ( 1st ` x ) ) -> V e. ( _V X. _V ) )
22 7 21 syl 
 |-  ( x e. ( V F K ) -> V e. ( _V X. _V ) )
23 22 exlimiv 
 |-  ( E. x x e. ( V F K ) -> V e. ( _V X. _V ) )
24 2 23 sylbi 
 |-  ( -. ( V F K ) = (/) -> V e. ( _V X. _V ) )
25 24 con1i 
 |-  ( -. V e. ( _V X. _V ) -> ( V F K ) = (/) )