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 𝑍 )