Theorem 0mpo0

Description: A mapping operation with empty domain is empty. Generalization of mpo0 . (Contributed by AV, 27-Jan-2024)

	Ref	Expression
Assertion	0mpo0	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅ )

Proof

Step	Hyp	Ref	Expression
1		df-mpo	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) }
2		df-oprab	⊢ { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) } = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
3	1 2	eqtri	⊢ ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) }
4		nel02	⊢ ( 𝐴 = ∅ → ¬ 𝑥 ∈ 𝐴 )
5		nel02	⊢ ( 𝐵 = ∅ → ¬ 𝑦 ∈ 𝐵 )
6	4 5	orim12i	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) )
7		ianor	⊢ ( ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ↔ ( ¬ 𝑥 ∈ 𝐴 ∨ ¬ 𝑦 ∈ 𝐵 ) )
8	6 7	sylibr	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
9		simprl	⊢ ( ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) → ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) )
10	8 9	nsyl	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
11	10	nexdv	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
12	11	nexdv	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
13	12	nexdv	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
14	13	alrimiv	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ∀ 𝑤 ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
15		ab0	⊢ ( { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = ∅ ↔ ∀ 𝑤 ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) )
16	14 15	sylibr	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → { 𝑤 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑧 ( 𝑤 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑧 = 𝐶 ) ) } = ∅ )
17	3 16	syl5eq	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅ )