Detailed syntax breakdown of Definition df-image
Step | Hyp | Ref
| Expression |
1 | | cA |
. . 3
class 𝐴 |
2 | 1 | cimage 34121 |
. 2
class
Image𝐴 |
3 | | cvv 3430 |
. . . 4
class
V |
4 | 3, 3 | cxp 5586 |
. . 3
class (V
× V) |
5 | | cep 5493 |
. . . . . 6
class
E |
6 | 3, 5 | ctxp 34111 |
. . . . 5
class (V
⊗ E ) |
7 | 1 | ccnv 5587 |
. . . . . . 7
class ◡𝐴 |
8 | 5, 7 | ccom 5592 |
. . . . . 6
class ( E
∘ ◡𝐴) |
9 | 8, 3 | ctxp 34111 |
. . . . 5
class (( E
∘ ◡𝐴) ⊗ V) |
10 | 6, 9 | csymdif 4180 |
. . . 4
class ((V
⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)) |
11 | 10 | crn 5589 |
. . 3
class ran ((V
⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V)) |
12 | 4, 11 | cdif 3888 |
. 2
class ((V
× V) ∖ ran ((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) |
13 | 2, 12 | wceq 1541 |
1
wff Image𝐴 = ((V × V) ∖ ran
((V ⊗ E ) △ (( E ∘ ◡𝐴) ⊗ V))) |