vfinspss - New Foundations Explorer

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

Theorem vfinspss 4552

Description: If the universe is finite, then Sp_fin is a subset of its

raisings and the cardinality of the universe. Theorem X.1.59 of [Rosser] p. 534. (Contributed by SF, 29-Jan-2015.)

**Assertion**
Ref	Expression
vfinspss	Fin Sp_fin Sp_fin T_fin Nc_fin

Distinct variable group:

Proof of Theorem vfinspss Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfineq 4489	. . . . . . . . . . 11 T_fin T_fin
2	1	eqeq2d 2364	. . . . . . . . . 10 T_fin T_fin
3	2	cbvrexv 2837	. . . . . . . . 9 Sp_fin T_fin Sp_fin T_fin
4		vfinspsslem1 4551	. . . . . . . . . . . . 13 Fin $/\$ T_fin Sp_fin $/\$ Sp_fin $/\$ S_fin T_fin Sp_fin T_fin
5	4	expr 598	. . . . . . . . . . . 12 Fin $/\$ T_fin Sp_fin $/\$ Sp_fin S_fin T_fin Sp_fin T_fin
6		eleq1 2413	. . . . . . . . . . . . . . 15 T_fin Sp_fin T_fin Sp_fin
7	6	anbi2d 684	. . . . . . . . . . . . . 14 T_fin Fin $/\$ Sp_fin Fin $/\$ T_fin Sp_fin
8	7	anbi1d 685	. . . . . . . . . . . . 13 T_fin Fin $/\$ Sp_fin $/\$ Sp_fin Fin $/\$ T_fin Sp_fin $/\$ Sp_fin
9		sfineq2 4528	. . . . . . . . . . . . . 14 T_fin S_fin S_fin T_fin
10	9	imbi1d 308	. . . . . . . . . . . . 13 T_fin S_fin Sp_fin T_fin S_fin T_fin Sp_fin T_fin
11	8, 10	imbi12d 311	. . . . . . . . . . . 12 T_fin Fin $/\$ Sp_fin $/\$ Sp_fin S_fin Sp_fin T_fin Fin $/\$ T_fin Sp_fin $/\$ Sp_fin S_fin T_fin Sp_fin T_fin
12	5, 11	mpbiri 224	. . . . . . . . . . 11 T_fin Fin $/\$ Sp_fin $/\$ Sp_fin S_fin Sp_fin T_fin
13	12	com12 27	. . . . . . . . . 10 Fin $/\$ Sp_fin $/\$ Sp_fin T_fin S_fin Sp_fin T_fin
14	13	rexlimdva 2739	. . . . . . . . 9 Fin $/\$ Sp_fin Sp_fin T_fin S_fin Sp_fin T_fin
15	3, 14	syl5bi 208	. . . . . . . 8 Fin $/\$ Sp_fin Sp_fin T_fin S_fin Sp_fin T_fin
16		sfineq2 4528	. . . . . . . . . . . 12 Nc_fin S_fin S_fin Nc_fin
17	16	biimpa 470	. . . . . . . . . . 11 Nc_fin $/\$ S_fin S_fin Nc_fin
18		1cvsfin 4543	. . . . . . . . . . . 12 Fin S_fin Nc_fin 1_c Nc_fin
19		sfin111 4537	. . . . . . . . . . . . 13 S_fin Nc_fin 1_c Nc_fin $/\$ S_fin Nc_fin Nc_fin 1_c
20		tncveqnc1fin 4545	. . . . . . . . . . . . . . . 16 Fin T_fin Nc_fin Nc_fin 1_c
21	20	eqcomd 2358	. . . . . . . . . . . . . . 15 Fin Nc_fin 1_c T_fin Nc_fin
22		ncvspfin 4539	. . . . . . . . . . . . . . . 16 Nc_fin Sp_fin
23		tfineq 4489	. . . . . . . . . . . . . . . . . 18 Nc_fin T_fin T_fin Nc_fin
24	23	eqeq2d 2364	. . . . . . . . . . . . . . . . 17 Nc_fin Nc_fin 1_c T_fin Nc_fin 1_c T_fin Nc_fin
25	24	rspcev 2956	. . . . . . . . . . . . . . . 16 Nc_fin Sp_fin $/\$ Nc_fin 1_c T_fin Nc_fin Sp_fin Nc_fin 1_c T_fin
26	22, 25	mpan 651	. . . . . . . . . . . . . . 15 Nc_fin 1_c T_fin Nc_fin Sp_fin Nc_fin 1_c T_fin
27	21, 26	syl 15	. . . . . . . . . . . . . 14 Fin Sp_fin Nc_fin 1_c T_fin
28		eqeq1 2359	. . . . . . . . . . . . . . . . 17 Nc_fin 1_c Nc_fin 1_c T_fin T_fin
29	28	rexbidv 2636	. . . . . . . . . . . . . . . 16 Nc_fin 1_c Sp_fin Nc_fin 1_c T_fin Sp_fin T_fin
30	29	biimpd 198	. . . . . . . . . . . . . . 15 Nc_fin 1_c Sp_fin Nc_fin 1_c T_fin Sp_fin T_fin
31	30	com12 27	. . . . . . . . . . . . . 14 Sp_fin Nc_fin 1_c T_fin Nc_fin 1_c Sp_fin T_fin
32	27, 31	syl 15	. . . . . . . . . . . . 13 Fin Nc_fin 1_c Sp_fin T_fin
33	19, 32	syl5 28	. . . . . . . . . . . 12 Fin S_fin Nc_fin 1_c Nc_fin $/\$ S_fin Nc_fin Sp_fin T_fin
34	18, 33	mpand 656	. . . . . . . . . . 11 Fin S_fin Nc_fin Sp_fin T_fin
35	17, 34	syl5 28	. . . . . . . . . 10 Fin Nc_fin $/\$ S_fin Sp_fin T_fin
36	35	exp3a 425	. . . . . . . . 9 Fin Nc_fin S_fin Sp_fin T_fin
37	36	adantr 451	. . . . . . . 8 Fin $/\$ Sp_fin Nc_fin S_fin Sp_fin T_fin
38	15, 37	jaod 369	. . . . . . 7 Fin $/\$ Sp_fin Sp_fin T_fin $\/$ Nc_fin S_fin Sp_fin T_fin
39	38	imp3a 420	. . . . . 6 Fin $/\$ Sp_fin Sp_fin T_fin $\/$ Nc_fin $/\$ S_fin Sp_fin T_fin
40		elun 3221	. . . . . . . 8 Sp_fin T_fin Nc_fin Sp_fin T_fin $\/$ Nc_fin
41		vex 2863	. . . . . . . . . 10
42		eqeq1 2359	. . . . . . . . . . 11 T_fin T_fin
43	42	rexbidv 2636	. . . . . . . . . 10 Sp_fin T_fin Sp_fin T_fin
44	41, 43	elab 2986	. . . . . . . . 9 Sp_fin T_fin Sp_fin T_fin
45	41	elsnc 3757	. . . . . . . . 9 Nc_fin Nc_fin
46	44, 45	orbi12i 507	. . . . . . . 8 Sp_fin T_fin $\/$ Nc_fin Sp_fin T_fin $\/$ Nc_fin
47	40, 46	bitri 240	. . . . . . 7 Sp_fin T_fin Nc_fin Sp_fin T_fin $\/$ Nc_fin
48	47	anbi1i 676	. . . . . 6 Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin $\/$ Nc_fin $/\$ S_fin
49		vex 2863	. . . . . . 7
50		eqeq1 2359	. . . . . . . 8 T_fin T_fin
51	50	rexbidv 2636	. . . . . . 7 Sp_fin T_fin Sp_fin T_fin
52	49, 51	elab 2986	. . . . . 6 Sp_fin T_fin Sp_fin T_fin
53	39, 48, 52	3imtr4g 261	. . . . 5 Fin $/\$ Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin
54		ssun1 3427	. . . . . 6 Sp_fin T_fin Sp_fin T_fin Nc_fin
55	54	sseli 3270	. . . . 5 Sp_fin T_fin Sp_fin T_fin Nc_fin
56	53, 55	syl6 29	. . . 4 Fin $/\$ Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin Nc_fin
57	56	alrimiv 1631	. . 3 Fin $/\$ Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin Nc_fin
58	57	ralrimiva 2698	. 2 Fin Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin Nc_fin
59		vex 2863	. . . . . . . . 9
60	59	elimak 4260	. . . . . . . 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
61		df-rex 2621	. . . . . . . . 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
62		elpw1 4145	. . . . . . . . . . . . 13 ₁ Sp_fin Sp_fin
63	62	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
64		r19.41v 2765	. . . . . . . . . . . 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
65	63, 64	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
66	65	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
67		rexcom4 2879	. . . . . . . . . 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
68	66, 67	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
69	61, 68	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
70	60, 69	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
71		snex 4112	. . . . . . . . . 10
72		opkeq1 4060	. . . . . . . . . . 11
73	72	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
74	71, 73	ceqsexv 2895	. . . . . . . . 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
75		vex 2863	. . . . . . . . . 10
76	75, 59	eqtfinrelk 4487	. . . . . . . . 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
77	74, 76	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
78	77	rexbii 2640	. . . . . . 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
79	70, 78	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
80	79	eqabi 2465	. . . . 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
81		tfinrelkex 4488	. . . . . 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
82		spfinex 4538	. . . . . . 7 Sp_fin
83	82	pw1ex 4304	. . . . . 6 ₁ Sp_fin
84	81, 83	imakex 4301	. . . . 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
85	80, 84	eqeltrri 2424	. . . 4 Sp_fin T_fin
86		snex 4112	. . . 4 Nc_fin
87	85, 86	unex 4107	. . 3 Sp_fin T_fin Nc_fin
88		ssun2 3428	. . . 4 Nc_fin Sp_fin T_fin Nc_fin
89		ncfinex 4473	. . . . 5 Nc_fin
90	89	snid 3761	. . . 4 Nc_fin Nc_fin
91	88, 90	sselii 3271	. . 3 Nc_fin Sp_fin T_fin Nc_fin
92		spfininduct 4541	. . 3 Sp_fin T_fin Nc_fin $/\$ Nc_fin Sp_fin T_fin Nc_fin $/\$ Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin Nc_fin Sp_fin Sp_fin T_fin Nc_fin
93	87, 91, 92	mp3an12 1267	. 2 Sp_fin Sp_fin T_fin Nc_fin $/\$ S_fin Sp_fin T_fin Nc_fin Sp_fin Sp_fin T_fin Nc_fin
94	58, 93	syl 15	1 Fin Sp_fin Sp_fin T_fin Nc_fin

Colors of variables: wff setvar class

Syntax hints:

wi 4 $\/$ wo 357 $/\$ wa 358

wal 1540

wex 1541

wceq 1642

wcel 1710

cab 2339

wral 2615

wrex 2616

cvv 2860 ∼ ccompl 3206

cdif 3207

cun 3208

cin 3209

csymdif 3210

wss 3258

c0 3551

cpw 3723

csn 3738

copk 4058 1_cc1c 4135

₁ cpw1 4136

_k cxpk 4175

_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178

_kcimak 4180 SI_k csik 4182 S_k cssetk 4184

_k cidk 4185 Nn cnnc 4374 Fin cfin 4377 Nc_fin cncfin 4435 T_fin ctfin 4436 S_fin wsfin 4439 Sp_fin cspfin 4440

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-13 1712 ax-14 1714 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-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 2479 df-ne 2519 df-ral 2620 df-rex 2621 df-reu 2622 df-rmo 2623 df-rab 2624 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-pss 3262 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-idk 4196 df-iota 4340 df-0c 4378 df-addc 4379 df-nnc 4380 df-fin 4381 df-lefin 4441 df-ltfin 4442 df-ncfin 4443 df-tfin 4444 df-sfin 4447 df-spfin 4448

This theorem is referenced by: vfinspeqtncv 4554

W3C validator