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