Definition df-clos1 5874

Description: Define the closure operation. A modified version of the definition from [Rosser] p. 245. (Contributed by SF, 11-Feb-2015.)

Assertion

Ref	Expression
df-clos1	⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}

Distinct variable groups:   S,a   R,a

Detailed syntax breakdown of Definition df-clos1

Step	Hyp	Ref	Expression
1		cS	. . 3 class S
2		cR	. . 3 class R
3	1, 2	cclos1 5873	. 2 class Clos1 (S, R)
4		va	. . . . . . 7 setvar a
5	4	cv 1641	. . . . . 6 class a
6	1, 5	wss 3258	. . . . 5 wff S ⊆ a
7	2, 5	cima 4723	. . . . . 6 class (R “ a)
8	7, 5	wss 3258	. . . . 5 wff (R “ a) ⊆ a
9	6, 8	wa 358	. . . 4 wff (S ⊆ a ∧ (R “ a) ⊆ a)
10	9, 4	cab 2339	. . 3 class {a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}
11	10	cint 3927	. 2 class ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}
12	3, 11	wceq 1642	1 wff Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)}

This definition is referenced by:  clos1eq1  5875  clos1eq2  5876  clos1ex  5877  clos1base  5879  clos1conn  5880  clos1induct  5881  dfnnc3  5886  nchoicelem10  6299