Detailed syntax breakdown of Definition df-apply
| Step | Hyp | Ref
| Expression |
|---|
| 1 | | capply 33306 |
. 2
class
Apply |
| 2 | | cbigcup 33295 |
. . . 4
class Bigcup |
| 3 | 2, 2 | ccom 5559 |
. . 3
class ( Bigcup ∘ Bigcup
) |
| 4 | | cvv 3494 |
. . . . . 6
class
V |
| 5 | 4, 4 | cxp 5553 |
. . . . 5
class (V
× V) |
| 6 | | cep 5464 |
. . . . . . . 8
class
E |
| 7 | 4, 6 | ctxp 33291 |
. . . . . . 7
class (V
⊗ E ) |
| 8 | | csingles 33300 |
. . . . . . . . 9
class Singletons |
| 9 | 6, 8 | cres 5557 |
. . . . . . . 8
class ( E
↾ Singletons ) |
| 10 | 9, 4 | ctxp 33291 |
. . . . . . 7
class (( E
↾ Singletons ) ⊗ V) |
| 11 | 7, 10 | csymdif 4218 |
. . . . . 6
class ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V)) |
| 12 | 11 | crn 5556 |
. . . . 5
class ran ((V
⊗ E ) △ (( E ↾ Singletons )
⊗ V)) |
| 13 | 5, 12 | cdif 3933 |
. . . 4
class ((V
× V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) |
| 14 | | csingle 33299 |
. . . . . 6
class
Singleton |
| 15 | | cimg 33303 |
. . . . . 6
class
Img |
| 16 | 14, 15 | ccom 5559 |
. . . . 5
class
(Singleton ∘ Img) |
| 17 | | cid 5459 |
. . . . . 6
class
I |
| 18 | 17, 14 | cpprod 33292 |
. . . . 5
class pprod( I
, Singleton) |
| 19 | 16, 18 | ccom 5559 |
. . . 4
class
((Singleton ∘ Img) ∘ pprod( I , Singleton)) |
| 20 | 13, 19 | ccom 5559 |
. . 3
class (((V
× V) ∖ ran ((V ⊗ E ) △ (( E ↾ Singletons ) ⊗ V))) ∘ ((Singleton ∘
Img) ∘ pprod( I , Singleton))) |
| 21 | 3, 20 | ccom 5559 |
. 2
class (( Bigcup ∘ Bigcup )
∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E ↾
Singletons ) ⊗ V))) ∘ ((Singleton
∘ Img) ∘ pprod( I , Singleton)))) |
| 22 | 1, 21 | wceq 1537 |
1
wff Apply =
(( Bigcup ∘ Bigcup
) ∘ (((V × V) ∖ ran ((V ⊗ E ) △ (( E
↾ Singletons ) ⊗ V))) ∘
((Singleton ∘ Img) ∘ pprod( I , Singleton)))) |
