This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
	Assertion	cantnfs	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )

Proof

Step	Hyp	Ref	Expression
1		cantnfs.s	⊢ 𝑆 = dom ( 𝐴 CNF 𝐵 )
2		cantnfs.a	⊢ ( 𝜑 → 𝐴 ∈ On )
3		cantnfs.b	⊢ ( 𝜑 → 𝐵 ∈ On )
4		eqid	⊢ { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ } = { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ }
5	4 2 3	cantnfdm	⊢ ( 𝜑 → dom ( 𝐴 CNF 𝐵 ) = { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
6	1 5	eqtrid	⊢ ( 𝜑 → 𝑆 = { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ } )
7	6	eleq2d	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ } ) )
8		breq1	⊢ ( 𝑔 = 𝐹 → ( 𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅ ) )
9	8	elrab	⊢ ( 𝐹 ∈ { 𝑔 ∈ ( 𝐴 ↑_m 𝐵 ) ∣ 𝑔 finSupp ∅ } ↔ ( 𝐹 ∈ ( 𝐴 ↑_m 𝐵 ) ∧ 𝐹 finSupp ∅ ) )
10	7 9	bitrdi	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 ∈ ( 𝐴 ↑_m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ) )
11	2 3	elmapd	⊢ ( 𝜑 → ( 𝐹 ∈ ( 𝐴 ↑_m 𝐵 ) ↔ 𝐹 : 𝐵 ⟶ 𝐴 ) )
12	11	anbi1d	⊢ ( 𝜑 → ( ( 𝐹 ∈ ( 𝐴 ↑_m 𝐵 ) ∧ 𝐹 finSupp ∅ ) ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )
13	10 12	bitrd	⊢ ( 𝜑 → ( 𝐹 ∈ 𝑆 ↔ ( 𝐹 : 𝐵 ⟶ 𝐴 ∧ 𝐹 finSupp ∅ ) ) )