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 9680

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 2735	. . . . . 6 ⊢ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}
3		cantnfs.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ On)
4		cantnfs.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ On)
5	2, 3, 4	cantnfdm 9678	. . . . 5 ⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
6	1, 5	eqtrid 2782	. . . 4 ⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
7	6	eleq2d 2820	. . 3 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ 𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}))
8		breq1 5122	. . . 4 ⊢ (𝑔 = 𝐹 → (𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅))
9	8	elrab 3671	. . 3 ⊢ (𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅))
10	7, 9	bitrdi 287	. 2 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅)))
11	3, 4	elmapd 8854	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐴 ↑_m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
12	11	anbi1d 631	. 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 1540 ∈ wcel 2108 {crab 3415 ∅c0 4308 class class class wbr 5119 dom cdm 5654 Oncon0 6352 ⟶wf 6527 (class class class)co 7405 ↑_m cmap 8840 finSupp cfsupp 9373 CNF ccnf 9675

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-10 2141 ax-11 2157 ax-12 2177 ax-ext 2707 ax-rep 5249 ax-sep 5266 ax-nul 5276 ax-pow 5335 ax-pr 5402 ax-un 7729

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3an 1088 df-tru 1543 df-fal 1553 df-ex 1780 df-nf 1784 df-sb 2065 df-mo 2539 df-eu 2568 df-clab 2714 df-cleq 2727 df-clel 2809 df-nfc 2885 df-ne 2933 df-ral 3052 df-rex 3061 df-reu 3360 df-rab 3416 df-v 3461 df-sbc 3766 df-csb 3875 df-dif 3929 df-un 3931 df-in 3933 df-ss 3943 df-nul 4309 df-if 4501 df-pw 4577 df-sn 4602 df-pr 4604 df-op 4608 df-uni 4884 df-iun 4969 df-br 5120 df-opab 5182 df-mpt 5202 df-id 5548 df-xp 5660 df-rel 5661 df-cnv 5662 df-co 5663 df-dm 5664 df-rn 5665 df-res 5666 df-ima 5667 df-pred 6290 df-iota 6484 df-fun 6533 df-fn 6534 df-f 6535 df-f1 6536 df-fo 6537 df-f1o 6538 df-fv 6539 df-ov 7408 df-oprab 7409 df-mpo 7410 df-frecs 8280 df-wrecs 8311 df-recs 8385 df-rdg 8424 df-seqom 8462 df-map 8842 df-cnf 9676

This theorem is referenced by: cantnfcl 9681 cantnfle 9685 cantnflt 9686 cantnff 9688 cantnf0 9689 cantnfrescl 9690 cantnfp1lem1 9692 cantnfp1lem2 9693 cantnfp1lem3 9694 cantnfp1 9695 oemapvali 9698 cantnflem1a 9699 cantnflem1b 9700 cantnflem1c 9701 cantnflem1d 9702 cantnflem1 9703 cantnflem3 9705 cantnf 9707 cnfcomlem 9713 cnfcom 9714 cnfcom2lem 9715 cnfcom3lem 9717 cnfcom3 9718 cantnfub 43345 cantnfresb 43348 cantnf2 43349 naddcnff 43386 naddcnffo 43388 naddcnfcom 43390 naddcnfid1 43391 naddcnfid2 43392 naddcnfass 43393

W3C validator