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 A , y B E
2mpo0.u X A Y B X O Y = s C , t D F
Assertion 2mpo0 ¬ X A Y B S C T D S X O Y T =

Proof

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