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 9578

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 2737	. . . . . 6 ⊢ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}
3		cantnfs.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ On)
4		cantnfs.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ On)
5	2, 3, 4	cantnfdm 9576	. . . . 5 ⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
6	1, 5	eqtrid 2784	. . . 4 ⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
7	6	eleq2d 2823	. . 3 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ 𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}))
8		breq1 5089	. . . 4 ⊢ (𝑔 = 𝐹 → (𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅))
9	8	elrab 3635	. . 3 ⊢ (𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅))
10	7, 9	bitrdi 287	. 2 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅)))
11	3, 4	elmapd 8780	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐴 ↑_m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
12	11	anbi1d 632	. 2 ⊢ (𝜑 → ((𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
13	10, 12	bitrd 279	1 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 206 ∧ wa 395 = wceq 1542 ∈ wcel 2114 {crab 3390 ∅c0 4274 class class class wbr 5086 dom cdm 5624 Oncon0 6317 ⟶wf 6488 (class class class)co 7360 ↑_m cmap 8766 finSupp cfsupp 9267 CNF ccnf 9573

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1797 ax-4 1811 ax-5 1912 ax-6 1969 ax-7 2010 ax-8 2116 ax-9 2124 ax-10 2147 ax-11 2163 ax-12 2185 ax-ext 2709 ax-rep 5212 ax-sep 5231 ax-nul 5241 ax-pow 5302 ax-pr 5370 ax-un 7682

This theorem depends on definitions: df-bi 207 df-an 396 df-or 849 df-3an 1089 df-tru 1545 df-fal 1555 df-ex 1782 df-nf 1786 df-sb 2069 df-mo 2540 df-eu 2570 df-clab 2716 df-cleq 2729 df-clel 2812 df-nfc 2886 df-ne 2934 df-ral 3053 df-rex 3063 df-reu 3344 df-rab 3391 df-v 3432 df-sbc 3730 df-csb 3839 df-dif 3893 df-un 3895 df-in 3897 df-ss 3907 df-nul 4275 df-if 4468 df-pw 4544 df-sn 4569 df-pr 4571 df-op 4575 df-uni 4852 df-iun 4936 df-br 5087 df-opab 5149 df-mpt 5168 df-id 5519 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-ov 7363 df-oprab 7364 df-mpo 7365 df-frecs 8224 df-wrecs 8255 df-recs 8304 df-rdg 8342 df-seqom 8380 df-map 8768 df-cnf 9574

This theorem is referenced by: cantnfcl 9579 cantnfle 9583 cantnflt 9584 cantnff 9586 cantnf0 9587 cantnfrescl 9588 cantnfp1lem1 9590 cantnfp1lem2 9591 cantnfp1lem3 9592 cantnfp1 9593 oemapvali 9596 cantnflem1a 9597 cantnflem1b 9598 cantnflem1c 9599 cantnflem1d 9600 cantnflem1 9601 cantnflem3 9603 cantnf 9605 cnfcomlem 9611 cnfcom 9612 cnfcom2lem 9613 cnfcom3lem 9615 cnfcom3 9616 cantnfub 43767 cantnfresb 43770 cantnf2 43771 naddcnff 43808 naddcnffo 43810 naddcnfcom 43812 naddcnfid1 43813 naddcnfid2 43814 naddcnfass 43815

W3C validator