vfinspclt - New Foundations Explorer

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

Theorem vfinspclt 4552

Description: If the universe is finite, then Sp_fin is closed under T-raising. Theorem X.1.60 of [Rosser] p. 536. (Contributed by SF, 30-Jan-2015.)

**Assertion**
Ref	Expression
vfinspclt	⊢ ((V ∈ Fin ∧ X ∈ Sp_fin ) → T_fin X ∈ Sp_fin )

Proof of Theorem vfinspclt Dummy variables x y z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		tncveqnc1fin 4544	. . . . . 6 ⊢ (V ∈ Fin → T_fin Nc_fin V = Nc_fin 1_c)
2		1cspfin 4543	. . . . . 6 ⊢ (V ∈ Fin → Nc_fin 1_c ∈ Sp_fin )
3	1, 2	eqeltrd 2427	. . . . 5 ⊢ (V ∈ Fin → T_fin Nc_fin V ∈ Sp_fin )
4		ncfinex 4472	. . . . . 6 ⊢ Nc_fin V ∈ V
5		tfineq 4488	. . . . . . 7 ⊢ (x = Nc_fin V → T_fin x = T_fin Nc_fin V)
6	5	eleq1d 2419	. . . . . 6 ⊢ (x = Nc_fin V → ( T_fin x ∈ Sp_fin ↔ T_fin Nc_fin V ∈ Sp_fin ))
7	4, 6	elab 2985	. . . . 5 ⊢ ( Nc_fin V ∈ {x ∣ T_fin x ∈ Sp_fin } ↔ T_fin Nc_fin V ∈ Sp_fin )
8	3, 7	sylibr 203	. . . 4 ⊢ (V ∈ Fin → Nc_fin V ∈ {x ∣ T_fin x ∈ Sp_fin })
9		simprl 732	. . . . . . . . 9 ⊢ (((V ∈ Fin ∧ y ∈ Sp_fin ) ∧ ( T_fin y ∈ Sp_fin ∧ S_fin (z, y))) → T_fin y ∈ Sp_fin )
10		sfintfin 4532	. . . . . . . . . 10 ⊢ ( S_fin (z, y) → S_fin ( T_fin z, T_fin y))
11	10	ad2antll 709	. . . . . . . . 9 ⊢ (((V ∈ Fin ∧ y ∈ Sp_fin ) ∧ ( T_fin y ∈ Sp_fin ∧ S_fin (z, y))) → S_fin ( T_fin z, T_fin y))
12		spfinsfincl 4539	. . . . . . . . 9 ⊢ (( T_fin y ∈ Sp_fin ∧ S_fin ( T_fin z, T_fin y)) → T_fin z ∈ Sp_fin )
13	9, 11, 12	syl2anc 642	. . . . . . . 8 ⊢ (((V ∈ Fin ∧ y ∈ Sp_fin ) ∧ ( T_fin y ∈ Sp_fin ∧ S_fin (z, y))) → T_fin z ∈ Sp_fin )
14	13	ex 423	. . . . . . 7 ⊢ ((V ∈ Fin ∧ y ∈ Sp_fin ) → (( T_fin y ∈ Sp_fin ∧ S_fin (z, y)) → T_fin z ∈ Sp_fin ))
15		vex 2862	. . . . . . . . 9 ⊢ y ∈ V
16		tfineq 4488	. . . . . . . . . 10 ⊢ (x = y → T_fin x = T_fin y)
17	16	eleq1d 2419	. . . . . . . . 9 ⊢ (x = y → ( T_fin x ∈ Sp_fin ↔ T_fin y ∈ Sp_fin ))
18	15, 17	elab 2985	. . . . . . . 8 ⊢ (y ∈ {x ∣ T_fin x ∈ Sp_fin } ↔ T_fin y ∈ Sp_fin )
19	18	anbi1i 676	. . . . . . 7 ⊢ ((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) ↔ ( T_fin y ∈ Sp_fin ∧ S_fin (z, y)))
20		vex 2862	. . . . . . . 8 ⊢ z ∈ V
21		tfineq 4488	. . . . . . . . 9 ⊢ (x = z → T_fin x = T_fin z)
22	21	eleq1d 2419	. . . . . . . 8 ⊢ (x = z → ( T_fin x ∈ Sp_fin ↔ T_fin z ∈ Sp_fin ))
23	20, 22	elab 2985	. . . . . . 7 ⊢ (z ∈ {x ∣ T_fin x ∈ Sp_fin } ↔ T_fin z ∈ Sp_fin )
24	14, 19, 23	3imtr4g 261	. . . . . 6 ⊢ ((V ∈ Fin ∧ y ∈ Sp_fin ) → ((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) → z ∈ {x ∣ T_fin x ∈ Sp_fin }))
25	24	alrimiv 1631	. . . . 5 ⊢ ((V ∈ Fin ∧ y ∈ Sp_fin ) → ∀z((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) → z ∈ {x ∣ T_fin x ∈ Sp_fin }))
26	25	ralrimiva 2697	. . . 4 ⊢ (V ∈ Fin → ∀y ∈ Sp_fin ∀z((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) → z ∈ {x ∣ T_fin x ∈ Sp_fin }))
27		snex 4111	. . . . . . . . . 10 ⊢ {x} ∈ V
28	27	elimak 4259	. . . . . . . . 9 ⊢ ({x} ∈ (^◡_k(({{∅}} ×_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 ) ↔ ∃y ∈ Sp_fin ⟪y, {x}⟫ ∈ ^◡_k(({{∅}} ×_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))))
29	15, 27	opkelcnvk 4250	. . . . . . . . . . 11 ⊢ (⟪y, {x}⟫ ∈ ^◡_k(({{∅}} ×_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}, y⟫ ∈ (({{∅}} ×_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))))
30		vex 2862	. . . . . . . . . . . 12 ⊢ x ∈ V
31	30, 15	eqtfinrelk 4486	. . . . . . . . . . 11 ⊢ (⟪{x}, y⟫ ∈ (({{∅}} ×_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))) ↔ y = T_fin x)
32	29, 31	bitri 240	. . . . . . . . . 10 ⊢ (⟪y, {x}⟫ ∈ ^◡_k(({{∅}} ×_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))) ↔ y = T_fin x)
33	32	rexbii 2639	. . . . . . . . 9 ⊢ (∃y ∈ Sp_fin ⟪y, {x}⟫ ∈ ^◡_k(({{∅}} ×_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))) ↔ ∃y ∈ Sp_fin y = T_fin x)
34	28, 33	bitri 240	. . . . . . . 8 ⊢ ({x} ∈ (^◡_k(({{∅}} ×_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 ) ↔ ∃y ∈ Sp_fin y = T_fin x)
35	30	eluni1 4173	. . . . . . . 8 ⊢ (x ∈ ⋃₁(^◡_k(({{∅}} ×_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} ∈ (^◡_k(({{∅}} ×_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 ))
36		risset 2661	. . . . . . . 8 ⊢ ( T_fin x ∈ Sp_fin ↔ ∃y ∈ Sp_fin y = T_fin x)
37	34, 35, 36	3bitr4i 268	. . . . . . 7 ⊢ (x ∈ ⋃₁(^◡_k(({{∅}} ×_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_fin x ∈ Sp_fin )
38	37	abbi2i 2464	. . . . . 6 ⊢ ⋃₁(^◡_k(({{∅}} ×_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 ∣ T_fin x ∈ Sp_fin }
39		tfinrelkex 4487	. . . . . . . . 9 ⊢ (({{∅}} ×_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
40	39	cnvkex 4287	. . . . . . . 8 ⊢ ^◡_k(({{∅}} ×_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
41		spfinex 4537	. . . . . . . 8 ⊢ Sp_fin ∈ V
42	40, 41	imakex 4300	. . . . . . 7 ⊢ (^◡_k(({{∅}} ×_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
43	42	uni1ex 4293	. . . . . 6 ⊢ ⋃₁(^◡_k(({{∅}} ×_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
44	38, 43	eqeltrri 2424	. . . . 5 ⊢ {x ∣ T_fin x ∈ Sp_fin } ∈ V
45		spfininduct 4540	. . . . 5 ⊢ (({x ∣ T_fin x ∈ Sp_fin } ∈ V ∧ Nc_fin V ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ ∀y ∈ Sp_fin ∀z((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) → z ∈ {x ∣ T_fin x ∈ Sp_fin })) → Sp_fin ⊆ {x ∣ T_fin x ∈ Sp_fin })
46	44, 45	mp3an1 1264	. . . 4 ⊢ (( Nc_fin V ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ ∀y ∈ Sp_fin ∀z((y ∈ {x ∣ T_fin x ∈ Sp_fin } ∧ S_fin (z, y)) → z ∈ {x ∣ T_fin x ∈ Sp_fin })) → Sp_fin ⊆ {x ∣ T_fin x ∈ Sp_fin })
47	8, 26, 46	syl2anc 642	. . 3 ⊢ (V ∈ Fin → Sp_fin ⊆ {x ∣ T_fin x ∈ Sp_fin })
48	47	sselda 3273	. 2 ⊢ ((V ∈ Fin ∧ X ∈ Sp_fin ) → X ∈ {x ∣ T_fin x ∈ Sp_fin })
49		tfineq 4488	. . . . 5 ⊢ (x = X → T_fin x = T_fin X)
50	49	eleq1d 2419	. . . 4 ⊢ (x = X → ( T_fin x ∈ Sp_fin ↔ T_fin X ∈ Sp_fin ))
51	50	elabg 2986	. . 3 ⊢ (X ∈ Sp_fin → (X ∈ {x ∣ T_fin x ∈ Sp_fin } ↔ T_fin X ∈ Sp_fin ))
52	51	adantl 452	. 2 ⊢ ((V ∈ Fin ∧ X ∈ Sp_fin ) → (X ∈ {x ∣ T_fin x ∈ Sp_fin } ↔ T_fin X ∈ Sp_fin ))
53	48, 52	mpbid 201	1 ⊢ ((V ∈ Fin ∧ X ∈ Sp_fin ) → T_fin X ∈ Sp_fin )

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 176 ∧ wa 358 ∀wal 1540 = 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 ⋃₁cuni1 4133 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-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 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-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-ncfin 4442 df-tfin 4443 df-sfin 4446 df-spfin 4447

This theorem is referenced by: vfinspeqtncv 4553

W3C validator