cantnfs - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > cantnfs		Structured version Visualization version GIF version

Theorem cantnfs 9636

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

**Hypotheses**
Ref	Expression
cantnfs.s	⊢ 𝑆 = dom (𝐴 CNF 𝐵)
cantnfs.a	⊢ (𝜑 → 𝐴 ∈ On)
cantnfs.b	⊢ (𝜑 → 𝐵 ∈ On)

**Assertion**
Ref	Expression
cantnfs	⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))

Proof of Theorem cantnfs Dummy variable 𝑔 is distinct from all other variables.

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

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 209 ∧ wa 400 = wceq 1570 ∈ wcel 2143 {crab 3416 ∅c0 4287 class class class wbr 5110 dom cdm 5663 Oncon0 6362 ⟶wf 6534 (class class class)co 7412 ↑_m cmap 8825 finSupp cfsupp 9322 CNF ccnf 9631

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1825 ax-4 1839 ax-5 1940 ax-6 1997 ax-7 2038 ax-8 2145 ax-9 2153 ax-10 2176 ax-11 2192 ax-12 2213 ax-ext 2735 ax-rep 5239 ax-sep 5258 ax-nul 5270 ax-pow 5338 ax-pr 5406 ax-un 7734

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1810 df-nf 1814 df-sb 2097 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2838 df-nfc 2912 df-ne 2959 df-ral 3080 df-rex 3090 df-reu 3370 df-rab 3417 df-v 3457 df-sbc 3746 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-nul 4288 df-if 4489 df-pw 4565 df-sn 4591 df-pr 4593 df-op 4597 df-uni 4874 df-iun 4959 df-br 5111 df-opab 5175 df-mpt 5194 df-id 5558 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6304 df-iota 6494 df-fun 6540 df-fn 6541 df-f 6542 df-f1 6543 df-fo 6544 df-f1o 6545 df-fv 6546 df-ov 7415 df-oprab 7416 df-mpo 7417 df-frecs 8279 df-wrecs 8310 df-recs 8359 df-rdg 8398 df-seqom 8436 df-map 8827 df-cnf 9632

This theorem is referenced by: cantnfcl 9637 cantnfle 9641 cantnflt 9642 cantnff 9644 cantnf0 9645 cantnfrescl 9646 cantnfp1lem1 9648 cantnfp1lem2 9649 cantnfp1lem3 9650 cantnfp1 9651 oemapvali 9654 cantnflem1a 9655 cantnflem1b 9656 cantnflem1c 9657 cantnflem1d 9658 cantnflem1 9659 cantnflem3 9661 cantnf 9663 cnfcomlem 9669 cnfcom 9670 cnfcom2lem 9671 cnfcom3lem 9673 cnfcom3 9674 cantnfub 44028 cantnfresb 44031 cantnf2 44032 naddcnff 44069 naddcnffo 44071 naddcnfcom 44073 naddcnfid1 44074 naddcnfid2 44075 naddcnfass 44076

W3C validator