This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )