vfinspss - New Foundations Explorer

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

Theorem vfinspss 4551

Description: If the universe is finite, then Sp_fin is a subset of its T 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	⊢ (V ∈ Fin → Sp_fin ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))

Distinct variable group: x,a

Proof of Theorem vfinspss Dummy variables t w z n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tfineq 4488	. . . . . . . . . . 11 ⊢ (x = n → T_fin x = T_fin n)
2	1	eqeq2d 2364	. . . . . . . . . 10 ⊢ (x = n → (w = T_fin x ↔ w = T_fin n))
3	2	cbvrexv 2836	. . . . . . . . 9 ⊢ (∃x ∈ Sp_fin w = T_fin x ↔ ∃n ∈ Sp_fin w = T_fin n)
4		vfinspsslem1 4550	. . . . . . . . . . . . 13 ⊢ (((V ∈ Fin ∧ T_fin n ∈ Sp_fin ) ∧ (n ∈ Sp_fin ∧ S_fin (z, T_fin n))) → ∃x ∈ Sp_fin z = T_fin x)
5	4	expr 598	. . . . . . . . . . . 12 ⊢ (((V ∈ Fin ∧ T_fin n ∈ Sp_fin ) ∧ n ∈ Sp_fin ) → ( S_fin (z, T_fin n) → ∃x ∈ Sp_fin z = T_fin x))
6		eleq1 2413	. . . . . . . . . . . . . . 15 ⊢ (w = T_fin n → (w ∈ Sp_fin ↔ T_fin n ∈ Sp_fin ))
7	6	anbi2d 684	. . . . . . . . . . . . . 14 ⊢ (w = T_fin n → ((V ∈ Fin ∧ w ∈ Sp_fin ) ↔ (V ∈ Fin ∧ T_fin n ∈ Sp_fin )))
8	7	anbi1d 685	. . . . . . . . . . . . 13 ⊢ (w = T_fin n → (((V ∈ Fin ∧ w ∈ Sp_fin ) ∧ n ∈ Sp_fin ) ↔ ((V ∈ Fin ∧ T_fin n ∈ Sp_fin ) ∧ n ∈ Sp_fin )))
9		sfineq2 4527	. . . . . . . . . . . . . 14 ⊢ (w = T_fin n → ( S_fin (z, w) ↔ S_fin (z, T_fin n)))
10	9	imbi1d 308	. . . . . . . . . . . . 13 ⊢ (w = T_fin n → (( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x) ↔ ( S_fin (z, T_fin n) → ∃x ∈ Sp_fin z = T_fin x)))
11	8, 10	imbi12d 311	. . . . . . . . . . . 12 ⊢ (w = T_fin n → ((((V ∈ Fin ∧ w ∈ Sp_fin ) ∧ n ∈ Sp_fin ) → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)) ↔ (((V ∈ Fin ∧ T_fin n ∈ Sp_fin ) ∧ n ∈ Sp_fin ) → ( S_fin (z, T_fin n) → ∃x ∈ Sp_fin z = T_fin x))))
12	5, 11	mpbiri 224	. . . . . . . . . . 11 ⊢ (w = T_fin n → (((V ∈ Fin ∧ w ∈ Sp_fin ) ∧ n ∈ Sp_fin ) → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
13	12	com12 27	. . . . . . . . . 10 ⊢ (((V ∈ Fin ∧ w ∈ Sp_fin ) ∧ n ∈ Sp_fin ) → (w = T_fin n → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
14	13	rexlimdva 2738	. . . . . . . . 9 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → (∃n ∈ Sp_fin w = T_fin n → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
15	3, 14	syl5bi 208	. . . . . . . 8 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → (∃x ∈ Sp_fin w = T_fin x → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
16		sfineq2 4527	. . . . . . . . . . . 12 ⊢ (w = Nc_fin V → ( S_fin (z, w) ↔ S_fin (z, Nc_fin V)))
17	16	biimpa 470	. . . . . . . . . . 11 ⊢ ((w = Nc_fin V ∧ S_fin (z, w)) → S_fin (z, Nc_fin V))
18		1cvsfin 4542	. . . . . . . . . . . 12 ⊢ (V ∈ Fin → S_fin ( Nc_fin 1_c, Nc_fin V))
19		sfin111 4536	. . . . . . . . . . . . 13 ⊢ (( S_fin ( Nc_fin 1_c, Nc_fin V) ∧ S_fin (z, Nc_fin V)) → Nc_fin 1_c = z)
20		tncveqnc1fin 4544	. . . . . . . . . . . . . . . 16 ⊢ (V ∈ Fin → T_fin Nc_fin V = Nc_fin 1_c)
21	20	eqcomd 2358	. . . . . . . . . . . . . . 15 ⊢ (V ∈ Fin → Nc_fin 1_c = T_fin Nc_fin V)
22		ncvspfin 4538	. . . . . . . . . . . . . . . 16 ⊢ Nc_fin V ∈ Sp_fin
23		tfineq 4488	. . . . . . . . . . . . . . . . . 18 ⊢ (x = Nc_fin V → T_fin x = T_fin Nc_fin V)
24	23	eqeq2d 2364	. . . . . . . . . . . . . . . . 17 ⊢ (x = Nc_fin V → ( Nc_fin 1_c = T_fin x ↔ Nc_fin 1_c = T_fin Nc_fin V))
25	24	rspcev 2955	. . . . . . . . . . . . . . . 16 ⊢ (( Nc_fin V ∈ Sp_fin ∧ Nc_fin 1_c = T_fin Nc_fin V) → ∃x ∈ Sp_fin Nc_fin 1_c = T_fin x)
26	22, 25	mpan 651	. . . . . . . . . . . . . . 15 ⊢ ( Nc_fin 1_c = T_fin Nc_fin V → ∃x ∈ Sp_fin Nc_fin 1_c = T_fin x)
27	21, 26	syl 15	. . . . . . . . . . . . . 14 ⊢ (V ∈ Fin → ∃x ∈ Sp_fin Nc_fin 1_c = T_fin x)
28		eqeq1 2359	. . . . . . . . . . . . . . . . 17 ⊢ ( Nc_fin 1_c = z → ( Nc_fin 1_c = T_fin x ↔ z = T_fin x))
29	28	rexbidv 2635	. . . . . . . . . . . . . . . 16 ⊢ ( Nc_fin 1_c = z → (∃x ∈ Sp_fin Nc_fin 1_c = T_fin x ↔ ∃x ∈ Sp_fin z = T_fin x))
30	29	biimpd 198	. . . . . . . . . . . . . . 15 ⊢ ( Nc_fin 1_c = z → (∃x ∈ Sp_fin Nc_fin 1_c = T_fin x → ∃x ∈ Sp_fin z = T_fin x))
31	30	com12 27	. . . . . . . . . . . . . 14 ⊢ (∃x ∈ Sp_fin Nc_fin 1_c = T_fin x → ( Nc_fin 1_c = z → ∃x ∈ Sp_fin z = T_fin x))
32	27, 31	syl 15	. . . . . . . . . . . . 13 ⊢ (V ∈ Fin → ( Nc_fin 1_c = z → ∃x ∈ Sp_fin z = T_fin x))
33	19, 32	syl5 28	. . . . . . . . . . . 12 ⊢ (V ∈ Fin → (( S_fin ( Nc_fin 1_c, Nc_fin V) ∧ S_fin (z, Nc_fin V)) → ∃x ∈ Sp_fin z = T_fin x))
34	18, 33	mpand 656	. . . . . . . . . . 11 ⊢ (V ∈ Fin → ( S_fin (z, Nc_fin V) → ∃x ∈ Sp_fin z = T_fin x))
35	17, 34	syl5 28	. . . . . . . . . 10 ⊢ (V ∈ Fin → ((w = Nc_fin V ∧ S_fin (z, w)) → ∃x ∈ Sp_fin z = T_fin x))
36	35	exp3a 425	. . . . . . . . 9 ⊢ (V ∈ Fin → (w = Nc_fin V → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
37	36	adantr 451	. . . . . . . 8 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → (w = Nc_fin V → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
38	15, 37	jaod 369	. . . . . . 7 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → ((∃x ∈ Sp_fin w = T_fin x ∨ w = Nc_fin V) → ( S_fin (z, w) → ∃x ∈ Sp_fin z = T_fin x)))
39	38	imp3a 420	. . . . . 6 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → (((∃x ∈ Sp_fin w = T_fin x ∨ w = Nc_fin V) ∧ S_fin (z, w)) → ∃x ∈ Sp_fin z = T_fin x))
40		elun 3220	. . . . . . . 8 ⊢ (w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ↔ (w ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∨ w ∈ { Nc_fin V}))
41		vex 2862	. . . . . . . . . 10 ⊢ w ∈ V
42		eqeq1 2359	. . . . . . . . . . 11 ⊢ (a = w → (a = T_fin x ↔ w = T_fin x))
43	42	rexbidv 2635	. . . . . . . . . 10 ⊢ (a = w → (∃x ∈ Sp_fin a = T_fin x ↔ ∃x ∈ Sp_fin w = T_fin x))
44	41, 43	elab 2985	. . . . . . . . 9 ⊢ (w ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ↔ ∃x ∈ Sp_fin w = T_fin x)
45	41	elsnc 3756	. . . . . . . . 9 ⊢ (w ∈ { Nc_fin V} ↔ w = Nc_fin V)
46	44, 45	orbi12i 507	. . . . . . . 8 ⊢ ((w ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∨ w ∈ { Nc_fin V}) ↔ (∃x ∈ Sp_fin w = T_fin x ∨ w = Nc_fin V))
47	40, 46	bitri 240	. . . . . . 7 ⊢ (w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ↔ (∃x ∈ Sp_fin w = T_fin x ∨ w = Nc_fin V))
48	47	anbi1i 676	. . . . . 6 ⊢ ((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) ↔ ((∃x ∈ Sp_fin w = T_fin x ∨ w = Nc_fin V) ∧ S_fin (z, w)))
49		vex 2862	. . . . . . 7 ⊢ z ∈ V
50		eqeq1 2359	. . . . . . . 8 ⊢ (a = z → (a = T_fin x ↔ z = T_fin x))
51	50	rexbidv 2635	. . . . . . 7 ⊢ (a = z → (∃x ∈ Sp_fin a = T_fin x ↔ ∃x ∈ Sp_fin z = T_fin x))
52	49, 51	elab 2985	. . . . . 6 ⊢ (z ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ↔ ∃x ∈ Sp_fin z = T_fin x)
53	39, 48, 52	3imtr4g 261	. . . . 5 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → ((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x}))
54		ssun1 3426	. . . . . 6 ⊢ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})
55	54	sseli 3269	. . . . 5 ⊢ (z ∈ {a ∣ ∃x ∈ Sp_fin a = T_fin x} → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
56	53, 55	syl6 29	. . . 4 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → ((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})))
57	56	alrimiv 1631	. . 3 ⊢ ((V ∈ Fin ∧ w ∈ Sp_fin ) → ∀z((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})))
58	57	ralrimiva 2697	. 2 ⊢ (V ∈ Fin → ∀w ∈ Sp_fin ∀z((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})))
59		vex 2862	. . . . . . . . 9 ⊢ a ∈ V
60	59	elimak 4259	. . . . . . . 8 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
61		df-rex 2620	. . . . . . . . 9 ⊢ (∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
62		elpw1 4144	. . . . . . . . . . . . 13 ⊢ (t ∈ ℘₁ Sp_fin ↔ ∃x ∈ Sp_fin t = {x})
63	62	anbi1i 676	. . . . . . . . . . . 12 ⊢ ((t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ (∃x ∈ Sp_fin t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
64		r19.41v 2764	. . . . . . . . . . . 12 ⊢ (∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ (∃x ∈ Sp_fin t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
65	63, 64	bitr4i 243	. . . . . . . . . . 11 ⊢ ((t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
66	65	exbii 1582	. . . . . . . . . 10 ⊢ (∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃t∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
67		rexcom4 2878	. . . . . . . . . 10 ⊢ (∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃t∃x ∈ Sp_fin (t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
68	66, 67	bitr4i 243	. . . . . . . . 9 ⊢ (∃t(t ∈ ℘₁ Sp_fin ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
69	61, 68	bitri 240	. . . . . . . 8 ⊢ (∃t ∈ ℘₁ Sp_fin ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
70	60, 69	bitri 240	. . . . . . 7 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
71		snex 4111	. . . . . . . . . 10 ⊢ {x} ∈ V
72		opkeq1 4059	. . . . . . . . . . 11 ⊢ (t = {x} → ⟪t, a⟫ = ⟪{x}, a⟫)
73	72	eleq1d 2419	. . . . . . . . . 10 ⊢ (t = {x} → (⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ ⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))))
74	71, 73	ceqsexv 2894	. . . . . . . . 9 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))))
75		vex 2862	. . . . . . . . . 10 ⊢ x ∈ V
76	75, 59	eqtfinrelk 4486	. . . . . . . . 9 ⊢ (⟪{x}, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ↔ a = T_fin x)
77	74, 76	bitri 240	. . . . . . . 8 ⊢ (∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ a = T_fin x)
78	77	rexbii 2639	. . . . . . 7 ⊢ (∃x ∈ Sp_fin ∃t(t = {x} ∧ ⟪t, a⟫ ∈ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V)))) ↔ ∃x ∈ Sp_fin a = T_fin x)
79	70, 78	bitri 240	. . . . . 6 ⊢ (a ∈ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ↔ ∃x ∈ Sp_fin a = T_fin x)
80	79	abbi2i 2464	. . . . 5 ⊢ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) = {a ∣ ∃x ∈ Sp_fin a = T_fin x}
81		tfinrelkex 4487	. . . . . 6 ⊢ (({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) ∈ V
82		spfinex 4537	. . . . . . 7 ⊢ Sp_fin ∈ V
83	82	pw1ex 4303	. . . . . 6 ⊢ ℘₁ Sp_fin ∈ V
84	81, 83	imakex 4300	. . . . 5 ⊢ ((({{∅}} ×_k {∅}) ∪ ( ∼ (( Ins2_k S_k ⊕ Ins3_k (( Ins3_k ^◡_k S_k ∖ Ins2_k (( Ins2_k (( Nn ×_k V) ∩ (( Ins2_k SI_k S_k ∩ Ins3_k (( Ins3_k SI_k ((℘1_c ×_k V) ∖ (( 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 I_k ) “_k ℘₁1_c)) “_k ℘₁1_c)) “_k ℘₁℘₁1_c) ∖ ({{∅}} ×_k V))) “_k ℘₁ Sp_fin ) ∈ V
85	80, 84	eqeltrri 2424	. . . 4 ⊢ {a ∣ ∃x ∈ Sp_fin a = T_fin x} ∈ V
86		snex 4111	. . . 4 ⊢ { Nc_fin V} ∈ V
87	85, 86	unex 4106	. . 3 ⊢ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∈ V
88		ssun2 3427	. . . 4 ⊢ { Nc_fin V} ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})
89		ncfinex 4472	. . . . 5 ⊢ Nc_fin V ∈ V
90	89	snid 3760	. . . 4 ⊢ Nc_fin V ∈ { Nc_fin V}
91	88, 90	sselii 3270	. . 3 ⊢ Nc_fin V ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})
92		spfininduct 4540	. . 3 ⊢ ((({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∈ V ∧ Nc_fin V ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ ∀w ∈ Sp_fin ∀z((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))) → Sp_fin ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
93	87, 91, 92	mp3an12 1267	. 2 ⊢ (∀w ∈ Sp_fin ∀z((w ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}) ∧ S_fin (z, w)) → z ∈ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V})) → Sp_fin ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))
94	58, 93	syl 15	1 ⊢ (V ∈ Fin → Sp_fin ⊆ ({a ∣ ∃x ∈ Sp_fin a = T_fin x} ∪ { Nc_fin V}))

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 2614 ∃wrex 2615 Vcvv 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 “_k cimak 4179 SI_k csik 4181 S_k cssetk 4183 I_k cidk 4184 Nn cnnc 4373 Fin cfin 4376 Nc_fin cncfin 4434 T_fin ctfin 4435 S_fin wsfin 4438 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: vfinspeqtncv 4553

W3C validator