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		eqeq1	⊢ ( 𝑧 = 𝑣 → ( 𝑧 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ↔ 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ) )
16	15	anbi1d	⊢ ( 𝑧 = 𝑣 → ( ( 𝑧 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ↔ ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ) )
17	16	3exbidv	⊢ ( 𝑧 = 𝑣 → ( ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑧 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ↔ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) ) )
18	17	ab0w	⊢ ( { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑧 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) } = ∅ ↔ ∀ 𝑣 ¬ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑣 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) )
19	14 18	sylibr	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → { 𝑧 ∣ ∃ 𝑥 ∃ 𝑦 ∃ 𝑤 ( 𝑧 = ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑤 ⟩ ∧ ( ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐵 ) ∧ 𝑤 = 𝐶 ) ) } = ∅ )
20	3 19	eqtrid	⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅ )