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 ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐸 )
2mpo0.u ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) )
Assertion 2mpo0 ( ¬ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )

Proof

Step Hyp Ref Expression
1 2mpo0.o ⊢ 𝑂 = ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐸 )
2 2mpo0.u ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) )
3 ianor ⊢ ( ¬ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) ↔ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∨ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) )
4 1 mpondm0 ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑋 𝑂 𝑌 ) = ∅ )
5 4 oveqd ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ( 𝑆 ∅ 𝑇 ) )
6 0ov ⊢ ( 𝑆 ∅ 𝑇 ) = ∅
7 5 6 eqtrdi ⊢ ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )
8 notnotb ⊢ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ↔ ¬ ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) )
9 2 adantr ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑋 𝑂 𝑌 ) = ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) )
10 9 oveqd ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ( 𝑆 ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) 𝑇 ) )
11 eqid ⊢ ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) = ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 )
12 11 mpondm0 ⊢ ( ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) → ( 𝑆 ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) 𝑇 ) = ∅ )
13 12 adantl ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑠 ∈ 𝐶 , 𝑡 ∈ 𝐷 ↦ 𝐹 ) 𝑇 ) = ∅ )
14 10 13 eqtrd ⊢ ( ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )
15 8 14 sylanbr ⊢ ( ( ¬ ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )
16 7 15 jaoi3 ⊢ ( ( ¬ ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∨ ¬ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )
17 3 16 sylbi ⊢ ( ¬ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )