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

Metamath Proof Explorer

Theorem supp0

Description: The support of the empty set is the empty set. (Contributed by AV, 12-Apr-2019)

Ref Expression
Assertion supp0 ( 𝑍 ∈ 𝑊 → ( ∅ supp 𝑍 ) = ∅ )

Proof

Step Hyp Ref Expression
1 0ex ⊢ ∅ ∈ V
2 suppval ⊢ ( ( ∅ ∈ V ∧ 𝑍 ∈ 𝑊 ) → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
3 1 2 mpan ⊢ ( 𝑍 ∈ 𝑊 → ( ∅ supp 𝑍 ) = { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
4 dm0 ⊢ dom ∅ = ∅
5 rabeq ⊢ ( dom ∅ = ∅ → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
6 4 5 mp1i ⊢ ( 𝑍 ∈ 𝑊 → { 𝑖 ∈ dom ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } )
7 rab0 ⊢ { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅
8 7 a1i ⊢ ( 𝑍 ∈ 𝑊 → { 𝑖 ∈ ∅ ∣ ( ∅ “ { 𝑖 } ) ≠ { 𝑍 } } = ∅ )
9 3 6 8 3eqtrd ⊢ ( 𝑍 ∈ 𝑊 → ( ∅ supp 𝑍 ) = ∅ )