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 >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) }
2 df-oprab 
 |-  { <. <. x , y >. , w >. | ( ( x e. A /\ y e. B ) /\ w = C ) } = { z | E. x E. y E. w ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) }
3 1 2 eqtri 
 |-  ( x e. A , y e. B |-> C ) = { z | E. x E. y E. w ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = 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 
 |-  ( ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) -> ( x e. A /\ y e. B ) )
10 8 9 nsyl 
 |-  ( ( A = (/) \/ B = (/) ) -> -. ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
11 10 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
12 11 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. y E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
13 12 nexdv 
 |-  ( ( A = (/) \/ B = (/) ) -> -. E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
14 13 alrimiv 
 |-  ( ( A = (/) \/ B = (/) ) -> A. v -. E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
15 eqeq1 
 |-  ( z = v -> ( z = <. <. x , y >. , w >. <-> v = <. <. x , y >. , w >. ) )
16 15 anbi1d 
 |-  ( z = v -> ( ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) <-> ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) ) )
17 16 3exbidv 
 |-  ( z = v -> ( E. x E. y E. w ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) <-> E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) ) )
18 17 ab0w 
 |-  ( { z | E. x E. y E. w ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) } = (/) <-> A. v -. E. x E. y E. w ( v = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) )
19 14 18 sylibr 
 |-  ( ( A = (/) \/ B = (/) ) -> { z | E. x E. y E. w ( z = <. <. x , y >. , w >. /\ ( ( x e. A /\ y e. B ) /\ w = C ) ) } = (/) )
20 3 19 eqtrid 
 |-  ( ( A = (/) \/ B = (/) ) -> ( x e. A , y e. B |-> C ) = (/) )