This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 2mpo0

Description: If the operation value of the operation value of two nested maps-to notation is not empty, all involved arguments belong to the corresponding base classes of the maps-to notations. (Contributed by AV, 21-May-2021)

Ref Expression
Hypotheses 2mpo0.o 
|- O = ( x e. A , y e. B |-> E )
2mpo0.u 
|- ( ( X e. A /\ Y e. B ) -> ( X O Y ) = ( s e. C , t e. D |-> F ) )
Assertion 2mpo0 
|- ( -. ( ( X e. A /\ Y e. B ) /\ ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )

Proof

Step Hyp Ref Expression
1 2mpo0.o 
 |-  O = ( x e. A , y e. B |-> E )
2 2mpo0.u 
 |-  ( ( X e. A /\ Y e. B ) -> ( X O Y ) = ( s e. C , t e. D |-> F ) )
3 ianor 
 |-  ( -. ( ( X e. A /\ Y e. B ) /\ ( S e. C /\ T e. D ) ) <-> ( -. ( X e. A /\ Y e. B ) \/ -. ( S e. C /\ T e. D ) ) )
4 1 mpondm0 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( X O Y ) = (/) )
5 4 oveqd 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( S ( X O Y ) T ) = ( S (/) T ) )
6 0ov 
 |-  ( S (/) T ) = (/)
7 5 6 eqtrdi 
 |-  ( -. ( X e. A /\ Y e. B ) -> ( S ( X O Y ) T ) = (/) )
8 notnotb 
 |-  ( ( X e. A /\ Y e. B ) <-> -. -. ( X e. A /\ Y e. B ) )
9 2 adantr 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( S e. C /\ T e. D ) ) -> ( X O Y ) = ( s e. C , t e. D |-> F ) )
10 9 oveqd 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = ( S ( s e. C , t e. D |-> F ) T ) )
11 eqid 
 |-  ( s e. C , t e. D |-> F ) = ( s e. C , t e. D |-> F )
12 11 mpondm0 
 |-  ( -. ( S e. C /\ T e. D ) -> ( S ( s e. C , t e. D |-> F ) T ) = (/) )
13 12 adantl 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( S e. C /\ T e. D ) ) -> ( S ( s e. C , t e. D |-> F ) T ) = (/) )
14 10 13 eqtrd 
 |-  ( ( ( X e. A /\ Y e. B ) /\ -. ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )
15 8 14 sylanbr 
 |-  ( ( -. -. ( X e. A /\ Y e. B ) /\ -. ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )
16 7 15 jaoi3 
 |-  ( ( -. ( X e. A /\ Y e. B ) \/ -. ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )
17 3 16 sylbi 
 |-  ( -. ( ( X e. A /\ Y e. B ) /\ ( S e. C /\ T e. D ) ) -> ( S ( X O Y ) T ) = (/) )