vfinncsp - New Foundations Explorer

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

Theorem vfinncsp 4554

Description: If the universe is finite, then the size of Sp_fin is equal to the successor of its T-raising. Theorem X.1.62 of [Rosser] p. 536. (Contributed by SF, 20-Jan-2015.)

**Assertion**
Ref	Expression
vfinncsp	Fin Nc_fin Sp_fin T_fin Nc_fin Sp_fin 1_c

Proof of Theorem vfinncsp Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		vfinspeqtncv 4553	. . 3 Fin Sp_fin Sp_fin T_fin Nc_fin
2		ncfineq 4473	. . 3 Sp_fin Sp_fin T_fin Nc_fin Nc_fin Sp_fin Nc_fin Sp_fin T_fin Nc_fin
3	1, 2	syl 15	. 2 Fin Nc_fin Sp_fin Nc_fin Sp_fin T_fin Nc_fin
4		vfinncvntsp 4549	. . . 4 Fin Nc_fin Sp_fin T_fin
5		disjsn 3786	. . . 4 Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin
6	4, 5	sylibr 203	. . 3 Fin Sp_fin T_fin Nc_fin
7		vex 2862	. . . . . . . . 9
8	7	elimak 4259	. . . . . . . 8 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k₁ Sp_fin ₁ Sp_fin _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
9		df-rex 2620	. . . . . . . . 9 ₁ Sp_fin _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k ₁ Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
10		elpw1 4144	. . . . . . . . . . . . 13 ₁ Sp_fin Sp_fin
11	10	anbi1i 676	. . . . . . . . . . . 12 ₁ Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
12		r19.41v 2764	. . . . . . . . . . . 12 Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
13	11, 12	bitr4i 243	. . . . . . . . . . 11 ₁ Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
14	13	exbii 1582	. . . . . . . . . 10 ₁ Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
15		rexcom4 2878	. . . . . . . . . 10 Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
16	14, 15	bitr4i 243	. . . . . . . . 9 ₁ Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
17	9, 16	bitri 240	. . . . . . . 8 ₁ Sp_fin _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
18	8, 17	bitri 240	. . . . . . 7 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k₁ Sp_fin Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
19		snex 4111	. . . . . . . . . 10
20		opkeq1 4059	. . . . . . . . . . 11
21	20	eleq1d 2419	. . . . . . . . . 10 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
22	19, 21	ceqsexv 2894	. . . . . . . . 9 $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
23		vex 2862	. . . . . . . . . 10
24	23, 7	eqtfinrelk 4486	. . . . . . . . 9 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
25	22, 24	bitri 240	. . . . . . . 8 $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k T_fin
26	25	rexbii 2639	. . . . . . 7 Sp_fin $/\$ _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k Sp_fin T_fin
27	18, 26	bitri 240	. . . . . 6 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k₁ Sp_fin Sp_fin T_fin
28	27	abbi2i 2464	. . . . 5 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k₁ Sp_fin Sp_fin T_fin
29		tfinrelkex 4487	. . . . . 6 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k
30		spfinex 4537	. . . . . . 7 Sp_fin
31	30	pw1ex 4303	. . . . . 6 ₁ Sp_fin
32	29, 31	imakex 4300	. . . . 5 _k ∼ Ins2_k S_k Ins3_k Ins3_k _k S_k Ins2_k Ins2_k Nn _k Ins2_k SI_k S_k Ins3_k Ins3_k SI_k 1_c _k Ins3_k S_k Ins2_k SI_k S_k _k₁ ₁ ₁ 1_c Ins2_k S_k _k₁ ₁ 1_c_k₁ ₁ ₁ 1_c Ins3_k _k _k₁ 1_c_k₁ 1_c_k₁ ₁ 1_c _k _k₁ Sp_fin
33	28, 32	eqeltrri 2424	. . . 4 Sp_fin T_fin
34		snex 4111	. . . . 5 Nc_fin
35		ncfindi 4475	. . . . 5 Fin $/\$ Sp_fin T_fin $/\$ Nc_fin $/\$ Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin
36	34, 35	mp3an2 1265	. . . 4 Fin $/\$ Sp_fin T_fin $/\$ Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin
37	33, 36	mpanl2 662	. . 3 Fin $/\$ Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin
38	6, 37	mpdan 649	. 2 Fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin
39		ncfinprop 4474	. . . . . 6 Fin $/\$ Sp_fin T_fin Nc_fin Sp_fin T_fin Nn $/\$ Sp_fin T_fin Nc_fin Sp_fin T_fin
40	33, 39	mpan2 652	. . . . 5 Fin Nc_fin Sp_fin T_fin Nn $/\$ Sp_fin T_fin Nc_fin Sp_fin T_fin
41	40	simpld 445	. . . 4 Fin Nc_fin Sp_fin T_fin Nn
42		ncfinprop 4474	. . . . . . 7 Fin $/\$ Sp_fin Nc_fin Sp_fin Nn $/\$ Sp_fin Nc_fin Sp_fin
43	30, 42	mpan2 652	. . . . . 6 Fin Nc_fin Sp_fin Nn $/\$ Sp_fin Nc_fin Sp_fin
44	43	simpld 445	. . . . 5 Fin Nc_fin Sp_fin Nn
45		tfincl 4492	. . . . 5 Nc_fin Sp_fin Nn T_fin Nc_fin Sp_fin Nn
46	44, 45	syl 15	. . . 4 Fin T_fin Nc_fin Sp_fin Nn
47	40	simprd 449	. . . 4 Fin Sp_fin T_fin Nc_fin Sp_fin T_fin
48		vfinspnn 4541	. . . . . 6 Fin Sp_fin Nn
49		difss 3393	. . . . . 6 Nn Nn
50	48, 49	syl6ss 3284	. . . . 5 Fin Sp_fin Nn
51	43	simprd 449	. . . . 5 Fin Sp_fin Nc_fin Sp_fin
52		tfinnn 4534	. . . . 5 Nc_fin Sp_fin Nn $/\$ Sp_fin Nn $/\$ Sp_fin Nc_fin Sp_fin Sp_fin T_fin T_fin Nc_fin Sp_fin
53	44, 50, 51, 52	syl3anc 1182	. . . 4 Fin Sp_fin T_fin T_fin Nc_fin Sp_fin
54		nnceleq 4430	. . . 4 Nc_fin Sp_fin T_fin Nn $/\$ T_fin Nc_fin Sp_fin Nn $/\$ Sp_fin T_fin Nc_fin Sp_fin T_fin $/\$ Sp_fin T_fin T_fin Nc_fin Sp_fin Nc_fin Sp_fin T_fin T_fin Nc_fin Sp_fin
55	41, 46, 47, 53, 54	syl22anc 1183	. . 3 Fin Nc_fin Sp_fin T_fin T_fin Nc_fin Sp_fin
56		ncfinex 4472	. . . 4 Nc_fin
57		ncfinsn 4476	. . . 4 Fin $/\$ Nc_fin Nc_fin Nc_fin 1_c
58	56, 57	mpan2 652	. . 3 Fin Nc_fin Nc_fin 1_c
59	55, 58	addceq12d 4391	. 2 Fin Nc_fin Sp_fin T_fin Nc_fin Nc_fin T_fin Nc_fin Sp_fin 1_c
60	3, 38, 59	3eqtrd 2389	1 Fin Nc_fin Sp_fin T_fin Nc_fin Sp_fin 1_c

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4 $/\$ wa 358

wex 1541

wceq 1642

wcel 1710

cab 2339

wrex 2615

cvv 2859 ∼ ccompl 3205

cdif 3206

cun 3207

cin 3208

csymdif 3209

wss 3257

c0 3550

cpw 3722

csn 3737

copk 4057 1_cc1c 4134

₁ cpw1 4135

_k cxpk 4174

_kccnvk 4175 Ins2_k cins2k 4176 Ins3_k cins3k 4177

_kcimak 4179 SI_k csik 4181 S_k cssetk 4183

_k cidk 4184 Nn cnnc 4373

cplc 4375 Fin cfin 4376 Nc_fin cncfin 4434 T_fin ctfin 4435 Sp_fin cspfin 4439

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

This theorem depends on definitions: df-bi 177 df-or 359 df-an 360 df-3or 935 df-3an 936 df-nan 1288 df-tru 1319 df-ex 1542 df-nf 1545 df-sb 1649 df-eu 2208 df-mo 2209 df-clab 2340 df-cleq 2346 df-clel 2349 df-nfc 2478 df-ne 2518 df-ral 2619 df-rex 2620 df-reu 2621 df-rmo 2622 df-rab 2623 df-v 2861 df-sbc 3047 df-nin 3211 df-compl 3212 df-in 3213 df-un 3214 df-dif 3215 df-symdif 3216 df-ss 3259 df-pss 3261 df-nul 3551 df-if 3663 df-pw 3724 df-sn 3741 df-pr 3742 df-uni 3892 df-int 3927 df-opk 4058 df-1c 4136 df-pw1 4137 df-uni1 4138 df-xpk 4185 df-cnvk 4186 df-ins2k 4187 df-ins3k 4188 df-imak 4189 df-cok 4190 df-p6 4191 df-sik 4192 df-ssetk 4193 df-imagek 4194 df-idk 4195 df-iota 4339 df-0c 4377 df-addc 4378 df-nnc 4379 df-fin 4380 df-lefin 4440 df-ltfin 4441 df-ncfin 4442 df-tfin 4443 df-sfin 4446 df-spfin 4447

This theorem is referenced by: vinf 4555

W3C validator