Detailed syntax breakdown of Definition df-funs
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cfuns 34639 |
. 2
class Funs |
| 2 | | cvv 3473 |
. . . . 5
class
V |
| 3 | 2, 2 | cxp 5667 |
. . . 4
class (V
× V) |
| 4 | 3 | cpw 4596 |
. . 3
class 𝒫
(V × V) |
| 5 | | cep 5572 |
. . . . 5
class
E |
| 6 | | c1st 7955 |
. . . . . . 7
class
1st |
| 7 | | cid 5566 |
. . . . . . . . 9
class
I |
| 8 | 2, 7 | cdif 3941 |
. . . . . . . 8
class (V
∖ I ) |
| 9 | | c2nd 7956 |
. . . . . . . 8
class
2nd |
| 10 | 8, 9 | ccom 5673 |
. . . . . . 7
class ((V
∖ I ) ∘ 2nd ) |
| 11 | 6, 10 | ctxp 34632 |
. . . . . 6
class
(1st ⊗ ((V ∖ I ) ∘ 2nd
)) |
| 12 | 5 | ccnv 5668 |
. . . . . 6
class ◡ E |
| 13 | 11, 12 | ccom 5673 |
. . . . 5
class
((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E ) |
| 14 | 5, 13 | ccom 5673 |
. . . 4
class ( E
∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E )) |
| 15 | 14 | cfix 34637 |
. . 3
class Fix ( E ∘ ((1st ⊗ ((V ∖ I
) ∘ 2nd )) ∘ ◡ E
)) |
| 16 | 4, 15 | cdif 3941 |
. 2
class
(𝒫 (V × V) ∖ Fix ( E
∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E ))) |
| 17 | 1, 16 | wceq 1541 |
1
wff Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I
) ∘ 2nd )) ∘ ◡ E
))) |
