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 = dom (A CNF B)$
		cantnfs.a	$⊢ φ \to A \in On$
		cantnfs.b	$⊢ φ \to B \in On$
	Assertion	cantnfs	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	$⊢ S = dom (A CNF B)$
2		cantnfs.a	$⊢ φ \to A \in On$
3		cantnfs.b	$⊢ φ \to B \in On$
4		eqid	$⊢ \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
5	4 2 3	cantnfdm	$⊢ φ \to dom (A CNF B) = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
6	1 5	eqtrid	$⊢ φ \to S = \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\}$
7	6	eleq2d	$⊢ φ \to (F \in S \leftrightarrow F \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\})$
8		breq1	$⊢ g = F \to ({finSupp}_{\emptyset} (g) \leftrightarrow {finSupp}_{\emptyset} (F))$
9	8	elrab	$⊢ F \in \{g \in (A^{B}) \| {finSupp}_{\emptyset} (g)\} \leftrightarrow (F \in (A^{B}) \land {finSupp}_{\emptyset} (F))$
10	7 9	bitrdi	$⊢ φ \to (F \in S \leftrightarrow (F \in (A^{B}) \land {finSupp}_{\emptyset} (F)))$
11	2 3	elmapd	$⊢ φ \to (F \in (A^{B}) \leftrightarrow F : B ⟶ A)$
12	11	anbi1d	$⊢ φ \to ((F \in (A^{B}) \land {finSupp}_{\emptyset} (F)) \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$
13	10 12	bitrd	$⊢ φ \to (F \in S \leftrightarrow (F : B ⟶ A \land {finSupp}_{\emptyset} (F)))$