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=xA,yBE
2mpo0.u XAYBXOY=sC,tDF
Assertion 2mpo0 ¬XAYBSCTDSXOYT=

Proof

Step Hyp Ref Expression
1 2mpo0.o O=xA,yBE
2 2mpo0.u XAYBXOY=sC,tDF
3 ianor ¬XAYBSCTD¬XAYB¬SCTD
4 1 mpondm0 ¬XAYBXOY=
5 4 oveqd ¬XAYBSXOYT=ST
6 0ov ST=
7 5 6 eqtrdi ¬XAYBSXOYT=
8 notnotb XAYB¬¬XAYB
9 2 adantr XAYB¬SCTDXOY=sC,tDF
10 9 oveqd XAYB¬SCTDSXOYT=SsC,tDFT
11 eqid sC,tDF=sC,tDF
12 11 mpondm0 ¬SCTDSsC,tDFT=
13 12 adantl XAYB¬SCTDSsC,tDFT=
14 10 13 eqtrd XAYB¬SCTDSXOYT=
15 8 14 sylanbr ¬¬XAYB¬SCTDSXOYT=
16 7 15 jaoi3 ¬XAYB¬SCTDSXOYT=
17 3 16 sylbi ¬XAYBSCTDSXOYT=