nncex - New Foundations Explorer

	New Foundations Explorer		< Previous Next > Nearby theorems
Mirrors > Home > NFE Home > Th. List > nncex		GIF 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 ∈ V

**Proof of Theorem nncex**
Step	Hyp	Ref	Expression
1		dfnnc2 4396	. 2 ⊢ Nn = ∩({x ∣ 0_c ∈ x} ∖ (( 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))) “_k 1_c))
2		setswithex 4323	. . . 4 ⊢ {x ∣ 0_c ∈ x} ∈ V
3		ssetkex 4295	. . . . . 6 ⊢ S_k ∈ V
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)) ∈ V
5		1cex 4143	. . . . . . . . . . . 12 ⊢ 1_c ∈ V
6	5	pw1ex 4304	. . . . . . . . . . 11 ⊢ 𝒫₁1_c ∈ V
7	6	pw1ex 4304	. . . . . . . . . 10 ⊢ 𝒫₁𝒫₁1_c ∈ V
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) ∈ V
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) ∈ V
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) ∈ V
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)) ∈ V
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))) ∈ V
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))) “_k 1_c) ∈ V
14	2, 13	difex 4108	. . 3 ⊢ ({x ∣ 0_c ∈ x} ∖ (( 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))) “_k 1_c)) ∈ V
15	14	intex 4321	. 2 ⊢ ∩({x ∣ 0_c ∈ x} ∖ (( 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))) “_k 1_c)) ∈ V
16	1, 15	eqeltri 2423	1 ⊢ Nn ∈ V

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∈ wcel 1710 {cab 2339 Vcvv 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 “_k cimak 4180 ∘_k ccomk 4181 SI_k csik 4182 Image_kcimagek 4183 S_k cssetk 4184 Nn cnnc 4374 0_cc0c 4375

This proof depends on 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 proof 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 used 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