Users' Mathboxes Mathbox for Scott Fenton < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-funs Structured version   Visualization version   GIF version

Definition df-funs 32289
Description: Define the class of all functions. See elfuns 32343 for membership. (Contributed by Scott Fenton, 18-Feb-2013.)
Assertion
Ref Expression
df-funs Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))

Detailed syntax breakdown of Definition df-funs
StepHypRef Expression
1 cfuns 32265 . 2 class Funs
2 cvv 3391 . . . . 5 class V
32, 2cxp 5309 . . . 4 class (V × V)
43cpw 4351 . . 3 class 𝒫 (V × V)
5 cep 5223 . . . . 5 class E
6 c1st 7396 . . . . . . 7 class 1st
7 cid 5218 . . . . . . . . 9 class I
82, 7cdif 3766 . . . . . . . 8 class (V ∖ I )
9 c2nd 7397 . . . . . . . 8 class 2nd
108, 9ccom 5315 . . . . . . 7 class ((V ∖ I ) ∘ 2nd )
116, 10ctxp 32258 . . . . . 6 class (1st ⊗ ((V ∖ I ) ∘ 2nd ))
125ccnv 5310 . . . . . 6 class E
1311, 12ccom 5315 . . . . 5 class ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )
145, 13ccom 5315 . . . 4 class ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))
1514cfix 32263 . . 3 class Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E ))
164, 15cdif 3766 . 2 class (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))
171, 16wceq 1637 1 wff Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd )) ∘ E )))
Colors of variables: wff setvar class
This definition is referenced by:  elfuns  32343
  Copyright terms: Public domain W3C validator