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=xV,y1stxC
Assertion mpoxopxnop0 ¬VV×VVFK=

Proof

Step Hyp Ref Expression
1 mpoxopn0yelv.f F=xV,y1stxC
2 neq0 ¬VFK=xxVFK
3 1 dmmpossx domFxVx×1stx
4 elfvdm xFVKVKdomF
5 df-ov VFK=FVK
6 4 5 eleq2s xVFKVKdomF
7 3 6 sselid xVFKVKxVx×1stx
8 fveq2 x=V1stx=1stV
9 8 opeliunxp2 VKxVx×1stxVVK1stV
10 eluni KdomVnKnndomV
11 ne0i ndomVdomV
12 11 ad2antlr KnndomVVVdomV
13 dmsnn0 VV×VdomV
14 12 13 sylibr KnndomVVVVV×V
15 14 ex KnndomVVVVV×V
16 15 exlimiv nKnndomVVVVV×V
17 10 16 sylbi KdomVVVVV×V
18 1stval 1stV=domV
19 17 18 eleq2s K1stVVVVV×V
20 19 impcom VVK1stVVV×V
21 9 20 sylbi VKxVx×1stxVV×V
22 7 21 syl xVFKVV×V
23 22 exlimiv xxVFKVV×V
24 2 23 sylbi ¬VFK=VV×V
25 24 con1i ¬VV×VVFK=