nncex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > nncex		Unicode version

Theorem nncex 4397

Description: The class of all finite cardinals is a set. (Contributed by SF, 14-Jan-2015.)

**Assertion**
Ref	Expression
nncex	Nn

**Proof of Theorem nncex**
Step	Hyp	Ref	Expression
1		dfnnc2 4396	. 2 Nn 0_c S_k S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k1_c
2		setswithex 4323	. . . 4 0_c
3		ssetkex 4295	. . . . . 6 S_k
4		addcexlem 4383	. . . . . . . . . 10 Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c
5		1cex 4143	. . . . . . . . . . . 12 1_c
6	5	pw1ex 4304	. . . . . . . . . . 11 ₁ 1_c
7	6	pw1ex 4304	. . . . . . . . . 10 ₁ ₁ 1_c
8	4, 7	imakex 4301	. . . . . . . . 9 Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
9	8	imagekex 4313	. . . . . . . 8 Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
10	9	sikex 4298	. . . . . . 7 SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
11	3, 10	cokex 4311	. . . . . 6 S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
12	3, 11	difex 4108	. . . . 5 S_k S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c
13	12, 5	imakex 4301	. . . 4 S_k S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k1_c
14	2, 13	difex 4108	. . 3 0_c S_k S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k1_c
15	14	intex 4321	. 2 0_c S_k S_k _k SI_k Image_k Ins3_k ∼ Ins3_k S_k Ins2_k S_k _k₁ ₁ 1_c Ins2_k Ins2_k S_k Ins2_k Ins3_k S_k Ins3_k SI_k SI_k S_k _k₁ ₁ ₁ ₁ 1_c_k₁ ₁ 1_c_k1_c
16	1, 15	eqeltri 2423	1 Nn

Colors of variables: wff setvar class

Syntax hints:

wcel 1710

cab 2339

cvv 2860 ∼ ccompl 3206

cdif 3207

cun 3208

cin 3209

csymdif 3210

cint 3927 1_cc1c 4135

₁ cpw1 4136 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180

_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 Nn cnnc 4374 0_cc0c 4375

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1546 ax-5 1557 ax-17 1616 ax-9 1654 ax-8 1675 ax-6 1729 ax-7 1734 ax-11 1746 ax-12 1925 ax-ext 2334 ax-nin 4079 ax-xp 4080 ax-cnv 4081 ax-1c 4082 ax-sset 4083 ax-si 4084 ax-ins2 4085 ax-ins3 4086 ax-typlower 4087 ax-sn 4088

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-v 2862 df-sbc 3048 df-nin 3212 df-compl 3213 df-in 3214 df-un 3215 df-dif 3216 df-symdif 3217 df-ss 3260 df-nul 3552 df-if 3664 df-pw 3725 df-sn 3742 df-pr 3743 df-uni 3893 df-int 3928 df-opk 4059 df-1c 4137 df-pw1 4138 df-uni1 4139 df-xpk 4186 df-cnvk 4187 df-ins2k 4188 df-ins3k 4189 df-imak 4190 df-cok 4191 df-p6 4192 df-sik 4193 df-ssetk 4194 df-imagek 4195 df-addc 4379 df-nnc 4380

This theorem is referenced by: finex 4398 peano5 4410 nnc0suc 4413 nncaddccl 4420 nndisjeq 4430 ltfinex 4465 ncfinraiselem2 4481 ncfinlowerlem1 4483 tfinrelkex 4488 evenfinex 4504 oddfinex 4505 evenodddisjlem1 4516 nnpweqlem1 4523 srelkex 4526 tfinnnlem1 4534 vfinspnn 4542 phiexg 4572 opexg 4588 proj1exg 4592 proj2exg 4593 phialllem1 4617 phialllem2 4618 setconslem5 4736 1stex 4740 swapex 4743 nclennlem1 6249 nmembers1lem1 6269 nncdiv3lem2 6277 nnc3n3p1 6279 nchoicelem16 6305 frecxp 6315

W3C validator