# Metamath Proof Explorer

## Theorem cantnfs

Description: Elementhood in the set of finitely supported functions from B to A . (Contributed by Mario Carneiro, 25-May-2015) (Revised by AV, 28-Jun-2019)

Ref Expression
Hypotheses cantnfs.s ${⊢}{S}=\mathrm{dom}\left({A}\mathrm{CNF}{B}\right)$
cantnfs.a ${⊢}{\phi }\to {A}\in \mathrm{On}$
cantnfs.b ${⊢}{\phi }\to {B}\in \mathrm{On}$
Assertion cantnfs ${⊢}{\phi }\to \left({F}\in {S}↔\left({F}:{B}⟶{A}\wedge {finSupp}_{\varnothing }\left({F}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 cantnfs.s ${⊢}{S}=\mathrm{dom}\left({A}\mathrm{CNF}{B}\right)$
2 cantnfs.a ${⊢}{\phi }\to {A}\in \mathrm{On}$
3 cantnfs.b ${⊢}{\phi }\to {B}\in \mathrm{On}$
4 eqid ${⊢}\left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}=\left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}$
5 4 2 3 cantnfdm ${⊢}{\phi }\to \mathrm{dom}\left({A}\mathrm{CNF}{B}\right)=\left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}$
6 1 5 syl5eq ${⊢}{\phi }\to {S}=\left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}$
7 6 eleq2d ${⊢}{\phi }\to \left({F}\in {S}↔{F}\in \left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}\right)$
8 breq1 ${⊢}{g}={F}\to \left({finSupp}_{\varnothing }\left({g}\right)↔{finSupp}_{\varnothing }\left({F}\right)\right)$
9 8 elrab ${⊢}{F}\in \left\{{g}\in \left({{A}}^{{B}}\right)|{finSupp}_{\varnothing }\left({g}\right)\right\}↔\left({F}\in \left({{A}}^{{B}}\right)\wedge {finSupp}_{\varnothing }\left({F}\right)\right)$
10 7 9 syl6bb ${⊢}{\phi }\to \left({F}\in {S}↔\left({F}\in \left({{A}}^{{B}}\right)\wedge {finSupp}_{\varnothing }\left({F}\right)\right)\right)$
11 2 3 elmapd ${⊢}{\phi }\to \left({F}\in \left({{A}}^{{B}}\right)↔{F}:{B}⟶{A}\right)$
12 11 anbi1d ${⊢}{\phi }\to \left(\left({F}\in \left({{A}}^{{B}}\right)\wedge {finSupp}_{\varnothing }\left({F}\right)\right)↔\left({F}:{B}⟶{A}\wedge {finSupp}_{\varnothing }\left({F}\right)\right)\right)$
13 10 12 bitrd ${⊢}{\phi }\to \left({F}\in {S}↔\left({F}:{B}⟶{A}\wedge {finSupp}_{\varnothing }\left({F}\right)\right)\right)$