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	⊢ ( ¬ ( ( 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐵 ) ∧ ( 𝑆 ∈ 𝐶 ∧ 𝑇 ∈ 𝐷 ) ) → ( 𝑆 ( 𝑋 𝑂 𝑌 ) 𝑇 ) = ∅ )