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 9645

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 2766	. . . . . 6 ⊢ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}
3		cantnfs.a	. . . . . 6 ⊢ (𝜑 → 𝐴 ∈ On)
4		cantnfs.b	. . . . . 6 ⊢ (𝜑 → 𝐵 ∈ On)
5	2, 3, 4	cantnfdm 9643	. . . . 5 ⊢ (𝜑 → dom (𝐴 CNF 𝐵) = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
6	1, 5	eqtrid 2813	. . . 4 ⊢ (𝜑 → 𝑆 = {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅})
7	6	eleq2d 2852	. . 3 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ 𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅}))
8		breq1 5117	. . . 4 ⊢ (𝑔 = 𝐹 → (𝑔 finSupp ∅ ↔ 𝐹 finSupp ∅))
9	8	elrab 3653	. . 3 ⊢ (𝐹 ∈ {𝑔 ∈ (𝐴 ↑_m 𝐵) ∣ 𝑔 finSupp ∅} ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅))
10	7, 9	bitrdi 290	. 2 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅)))
11	3, 4	elmapd 8846	. . 3 ⊢ (𝜑 → (𝐹 ∈ (𝐴 ↑_m 𝐵) ↔ 𝐹:𝐵⟶𝐴))
12	11	anbi1d 643	. 2 ⊢ (𝜑 → ((𝐹 ∈ (𝐴 ↑_m 𝐵) ∧ 𝐹 finSupp ∅) ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))
13	10, 12	bitrd 282	1 ⊢ (𝜑 → (𝐹 ∈ 𝑆 ↔ (𝐹:𝐵⟶𝐴 ∧ 𝐹 finSupp ∅)))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ↔ wb 209 ∧ wa 401 = wceq 1570 ∈ wcel 2146 {crab 3419 ∅c0 4289 class class class wbr 5114 dom cdm 5666 Oncon0 6367 ⟶wf 6539 (class class class)co 7423 ↑_m cmap 8833 finSupp cfsupp 9331 CNF ccnf 9640

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2738 ax-rep 5243 ax-sep 5262 ax-nul 5274 ax-pow 5341 ax-pr 5409 ax-un 7745

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2570 df-eu 2600 df-clab 2745 df-cleq 2758 df-clel 2841 df-nfc 2915 df-ne 2962 df-ral 3083 df-rex 3093 df-reu 3373 df-rab 3420 df-v 3460 df-sbc 3748 df-csb 3857 df-dif 3911 df-un 3913 df-in 3915 df-ss 3925 df-nul 4290 df-if 4493 df-pw 4569 df-sn 4595 df-pr 4597 df-op 4601 df-uni 4878 df-iun 4963 df-br 5115 df-opab 5179 df-mpt 5198 df-id 5561 df-xp 5672 df-rel 5673 df-cnv 5674 df-co 5675 df-dm 5676 df-rn 5677 df-res 5678 df-ima 5679 df-pred 6309 df-iota 6499 df-fun 6545 df-fn 6546 df-f 6547 df-f1 6548 df-fo 6549 df-f1o 6550 df-fv 6551 df-ov 7426 df-oprab 7427 df-mpo 7428 df-frecs 8287 df-wrecs 8318 df-recs 8367 df-rdg 8406 df-seqom 8444 df-map 8835 df-cnf 9641

This theorem is used by: cantnfcl 9646 cantnfle 9650 cantnflt 9651 cantnff 9653 cantnf0 9654 cantnfrescl 9655 cantnfp1lem1 9657 cantnfp1lem2 9658 cantnfp1lem3 9659 cantnfp1 9660 oemapvali 9663 cantnflem1a 9664 cantnflem1b 9665 cantnflem1c 9666 cantnflem1d 9667 cantnflem1 9668 cantnflem3 9670 cantnf 9672 cnfcomlem 9678 cnfcom 9679 cnfcom2lem 9680 cnfcom3lem 9682 cnfcom3 9683 cantnfub 44089 cantnfresb 44092 cantnf2 44093 naddcnff 44130 naddcnffo 44132 naddcnfcom 44134 naddcnfid1 44135 naddcnfid2 44136 naddcnfass 44137

W3C validator