Metamath Proof Explorer


Definition df-cap

Description: Define the little cap function. See brcap for its value. (Contributed by Scott Fenton, 17-Apr-2014)

Ref Expression
Assertion df-cap Cap = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V ) ) )

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccap Cap
1 cvv V
2 1 1 cxp ( V × V )
3 2 1 cxp ( ( V × V ) × V )
4 cep E
5 1 4 ctxp ( V ⊗ E )
6 c1st 1st
7 6 ccnv 1st
8 7 4 ccom ( 1st ∘ E )
9 c2nd 2nd
10 9 ccnv 2nd
11 10 4 ccom ( 2nd ∘ E )
12 8 11 cin ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) )
13 12 1 ctxp ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V )
14 5 13 csymdif ( ( V ⊗ E ) △ ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V ) )
15 14 crn ran ( ( V ⊗ E ) △ ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V ) )
16 3 15 cdif ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V ) ) )
17 0 16 wceq Cap = ( ( ( V × V ) × V ) ∖ ran ( ( V ⊗ E ) △ ( ( ( 1st ∘ E ) ∩ ( 2nd ∘ E ) ) ⊗ V ) ) )