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 = dom ( A CNF B )
	cantnfs.a	|- ( ph -> A e. On )
	cantnfs.b	|- ( ph -> B e. On )
Assertion	cantnfs	|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	|- S = dom ( A CNF B )
2		cantnfs.a	|- ( ph -> A e. On )
3		cantnfs.b	|- ( ph -> B e. On )
4		eqid	|- { g e. ( A ^m B ) | g finSupp (/) } = { g e. ( A ^m B ) | g finSupp (/) }
5	4 2 3	cantnfdm	|- ( ph -> dom ( A CNF B ) = { g e. ( A ^m B ) | g finSupp (/) } )
6	1 5	eqtrid	|- ( ph -> S = { g e. ( A ^m B ) | g finSupp (/) } )
7	6	eleq2d	|- ( ph -> ( F e. S <-> F e. { g e. ( A ^m B ) | g finSupp (/) } ) )
8		breq1	|- ( g = F -> ( g finSupp (/) <-> F finSupp (/) ) )
9	8	elrab	|- ( F e. { g e. ( A ^m B ) | g finSupp (/) } <-> ( F e. ( A ^m B ) /\ F finSupp (/) ) )
10	7 9	bitrdi	|- ( ph -> ( F e. S <-> ( F e. ( A ^m B ) /\ F finSupp (/) ) ) )
11	2 3	elmapd	|- ( ph -> ( F e. ( A ^m B ) <-> F : B --> A ) )
12	11	anbi1d	|- ( ph -> ( ( F e. ( A ^m B ) /\ F finSupp (/) ) <-> ( F : B --> A /\ F finSupp (/) ) ) )
13	10 12	bitrd	|- ( ph -> ( F e. S <-> ( F : B --> A /\ F finSupp (/) ) ) )