Detailed syntax breakdown of Definition df-funs
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | cfuns 34139 |
. 2
class Funs |
| 2 | | cvv 3432 |
. . . . 5
class
V |
| 3 | 2, 2 | cxp 5587 |
. . . 4
class (V
× V) |
| 4 | 3 | cpw 4533 |
. . 3
class 𝒫
(V × V) |
| 5 | | cep 5494 |
. . . . 5
class
E |
| 6 | | c1st 7829 |
. . . . . . 7
class
1st |
| 7 | | cid 5488 |
. . . . . . . . 9
class
I |
| 8 | 2, 7 | cdif 3884 |
. . . . . . . 8
class (V
∖ I ) |
| 9 | | c2nd 7830 |
. . . . . . . 8
class
2nd |
| 10 | 8, 9 | ccom 5593 |
. . . . . . 7
class ((V
∖ I ) ∘ 2nd ) |
| 11 | 6, 10 | ctxp 34132 |
. . . . . 6
class
(1st ⊗ ((V ∖ I ) ∘ 2nd
)) |
| 12 | 5 | ccnv 5588 |
. . . . . 6
class ◡ E |
| 13 | 11, 12 | ccom 5593 |
. . . . 5
class
((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E ) |
| 14 | 5, 13 | ccom 5593 |
. . . 4
class ( E
∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E )) |
| 15 | 14 | cfix 34137 |
. . 3
class Fix ( E ∘ ((1st ⊗ ((V ∖ I
) ∘ 2nd )) ∘ ◡ E
)) |
| 16 | 4, 15 | cdif 3884 |
. 2
class
(𝒫 (V × V) ∖ Fix ( E
∘ ((1st ⊗ ((V ∖ I ) ∘ 2nd ))
∘ ◡ E ))) |
| 17 | 1, 16 | wceq 1539 |
1
wff Funs = (𝒫 (V × V) ∖ Fix ( E ∘ ((1st ⊗ ((V ∖ I
) ∘ 2nd )) ∘ ◡ E
))) |
