vfinspclt - New Foundations Explorer

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

Theorem vfinspclt 4553

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 4545	. . . . . 6 ⊢ (V ∈ Fin → T_fin Nc_fin V = Nc_fin 1_c)
2		1cspfin 4544	. . . . . 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 4473	. . . . . 6 ⊢ Nc_fin V ∈ V
5		tfineq 4489	. . . . . . 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 2986	. . . . 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 4533	. . . . . . . . . 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 4540	. . . . . . . . 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 2863	. . . . . . . . 9 ⊢ y ∈ V
16		tfineq 4489	. . . . . . . . . 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 2986	. . . . . . . 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 2863	. . . . . . . 8 ⊢ z ∈ V
21		tfineq 4489	. . . . . . . . 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 2986	. . . . . . 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 2698	. . . 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 4112	. . . . . . . . . 10 ⊢ {x} ∈ V
28	27	elimak 4260	. . . . . . . . 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 4251	. . . . . . . . . . 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 2863	. . . . . . . . . . . 12 ⊢ x ∈ V
31	30, 15	eqtfinrelk 4487	. . . . . . . . . . 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 2640	. . . . . . . . 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 4174	. . . . . . . 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 2662	. . . . . . . 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 2465	. . . . . 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 4488	. . . . . . . . 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 4288	. . . . . . . 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 4538	. . . . . . . 8 ⊢ Sp_fin ∈ V
42	40, 41	imakex 4301	. . . . . . 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 4294	. . . . . 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 4541	. . . . 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 3274	. 2 ⊢ ((V ∈ Fin ∧ X ∈ Sp_fin ) → X ∈ {x ∣ T_fin x ∈ Sp_fin })
49		tfineq 4489	. . . . 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 2987	. . 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 2615 ∃wrex 2616 Vcvv 2860 ∼ ccompl 3206 ∖ cdif 3207 ∪ cun 3208 ∩ cin 3209 ⊕ csymdif 3210 ⊆ wss 3258 ∅c0 3551 ℘cpw 3723 {csn 3738 ⟪copk 4058 ⋃₁cuni1 4134 1_cc1c 4135 ℘₁cpw1 4136 ×_k cxpk 4175 ^◡_kccnvk 4176 Ins2_k cins2k 4177 Ins3_k cins3k 4178 “_k cimak 4180 SI_k csik 4182 S_k cssetk 4184 I_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-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-ncfin 4443 df-tfin 4444 df-sfin 4447 df-spfin 4448

This theorem is referenced by: vfinspeqtncv 4554

W3C validator