Metamath Proof Explorer

Theorem 0mpo0

Description: A mapping operation with empty domain is empty. Generalization of mpo0 . (Contributed by AV, 27-Jan-2024)

Ref Expression
Assertion 0mpo0 
|- ( ( A = (/) \/ B = (/) ) -> ( x e. A , y e. B |-> C ) = (/) )

Proof

Step Hyp Ref Expression
1 df-mpo 
 |-  ( x e. A , y e. B |-> C ) = { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) }
2 df-oprab 
 |-  { <. <. x , y >. , z >. | ( ( x e. A /\ y e. B ) /\ z = C ) } = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
3 1 2 eqtri 
 |-  ( x e. A , y e. B |-> C ) = { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) }
4 nel02 
 |-  ( A = (/) -> -. x e. A )
5 nel02 
 |-  ( B = (/) -> -. y e. B )
6 4 5 orim12i 
 |-  ( ( A = (/) \/ B = (/) ) -> ( -. x e. A \/ -. y e. B ) )
7 ianor 
 |-  ( -. ( x e. A /\ y e. B ) <-> ( -. x e. A \/ -. y e. B ) )
8 6 7 sylibr 
 |-  ( ( A = (/) \/ B = (/) ) -> -. ( x e. A /\ y e. B ) )
9 simprl 
 |-  ( ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) -> ( x e. A /\ y e. B ) )
10 8 9 nsyl 
 |-  ( ( A = (/) \/ B = (/) ) -> -. ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
11 10 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
12 11 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
13 12 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
14 13 alrimiv 
 |-  ( ( A = (/) \/ B = (/) ) -> A. w -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
15 ab0 
 |-  ( { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } = (/) <-> A. w -. E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) )
16 14 15 sylibr 
 |-  ( ( A = (/) \/ B = (/) ) -> { w | E. x E. y E. z ( w = <. <. x , y >. , z >. /\ ( ( x e. A /\ y e. B ) /\ z = C ) ) } = (/) )
17 3 16 syl5eq 
 |-  ( ( A = (/) \/ B = (/) ) -> ( x e. A , y e. B |-> C ) = (/) )