New Foundations Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > NFE Home > Th. List > df-clos1 | GIF version |
Description: Define the closure operation. A modified version of the definition from [Rosser] p. 245. (Contributed by SF, 11-Feb-2015.) |
Ref | Expression |
---|---|
df-clos1 | ⊢ Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)} |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cS | . . 3 class S | |
2 | cR | . . 3 class R | |
3 | 1, 2 | cclos1 5872 | . 2 class Clos1 (S, R) |
4 | va | . . . . . . 7 setvar a | |
5 | 4 | cv 1641 | . . . . . 6 class a |
6 | 1, 5 | wss 3257 | . . . . 5 wff S ⊆ a |
7 | 2, 5 | cima 4722 | . . . . . 6 class (R “ a) |
8 | 7, 5 | wss 3257 | . . . . 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 3926 | . 2 class ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)} |
12 | 3, 11 | wceq 1642 | 1 wff Clos1 (S, R) = ∩{a ∣ (S ⊆ a ∧ (R “ a) ⊆ a)} |
Colors of variables: wff setvar class |
This definition is referenced by: clos1eq1 5874 clos1eq2 5875 clos1ex 5876 clos1base 5878 clos1conn 5879 clos1induct 5880 dfnnc3 5885 nchoicelem10 6298 |
Copyright terms: Public domain | W3C validator |