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 ) = (/) )