This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ⊢ ( ( 𝐴 = ∅ ∨ 𝐵 = ∅ ) → ( 𝑥 ∈ 𝐴 , 𝑦 ∈ 𝐵 ↦ 𝐶 ) = ∅ )