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

Metamath Proof Explorer

Theorem snopfsupp

Description: A singleton containing an ordered pair is a finitely supported function. (Contributed by AV, 19-Jul-2019)

Ref Expression
Assertion snopfsupp ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 )

Proof

Step Hyp Ref Expression
1 snfi ⊢ { 𝑋 } ∈ Fin
2 snopsuppss ⊢ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ { 𝑋 }
3 1 2 pm3.2i ⊢ ( { 𝑋 } ∈ Fin ∧ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ { 𝑋 } )
4 ssfi ⊢ ( ( { 𝑋 } ∈ Fin ∧ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ⊆ { 𝑋 } ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ∈ Fin )
5 3 4 mp1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ∈ Fin )
6 funsng ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ) → Fun { ⟨ 𝑋 , 𝑌 ⟩ } )
7 6 3adant3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → Fun { ⟨ 𝑋 , 𝑌 ⟩ } )
8 snex ⊢ { ⟨ 𝑋 , 𝑌 ⟩ } ∈ V
9 8 a1i ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { ⟨ 𝑋 , 𝑌 ⟩ } ∈ V )
10 simp3 ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → 𝑍 ∈ 𝑈 )
11 funisfsupp ⊢ ( ( Fun { ⟨ 𝑋 , 𝑌 ⟩ } ∧ { ⟨ 𝑋 , 𝑌 ⟩ } ∈ V ∧ 𝑍 ∈ 𝑈 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 ↔ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ∈ Fin ) )
12 7 9 10 11 syl3anc ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → ( { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 ↔ ( { ⟨ 𝑋 , 𝑌 ⟩ } supp 𝑍 ) ∈ Fin ) )
13 5 12 mpbird ⊢ ( ( 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑊 ∧ 𝑍 ∈ 𝑈 ) → { ⟨ 𝑋 , 𝑌 ⟩ } finSupp 𝑍 )