Metamath Proof Explorer

Theorem brcap

Description: Binary relation form of the Cap function. (Contributed by Scott Fenton, 17-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

Ref Expression
Hypotheses brcap.1 
|- A e. _V
brcap.2 
|- B e. _V
brcap.3 
|- C e. _V
Assertion brcap 
|- ( <. A , B >. Cap C <-> C = ( A i^i B ) )

Proof

Step Hyp Ref Expression
1 brcap.1 
 |-  A e. _V
2 brcap.2 
 |-  B e. _V
3 brcap.3 
 |-  C e. _V
4 opex 
 |-  <. A , B >. e. _V
5 df-cap 
 |-  Cap = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) i^i ( `' 2nd o. _E ) ) (x) _V ) ) )
6 1 2 opelvv 
 |-  <. A , B >. e. ( _V X. _V )
7 brxp 
 |-  ( <. A , B >. ( ( _V X. _V ) X. _V ) C <-> ( <. A , B >. e. ( _V X. _V ) /\ C e. _V ) )
8 6 3 7 mpbir2an 
 |-  <. A , B >. ( ( _V X. _V ) X. _V ) C
9 epel 
 |-  ( x _E y <-> x e. y )
10 vex 
 |-  y e. _V
11 10 4 brcnv 
 |-  ( y `' 1st <. A , B >. <-> <. A , B >. 1st y )
12 1 2 br1steq 
 |-  ( <. A , B >. 1st y <-> y = A )
13 11 12 bitri 
 |-  ( y `' 1st <. A , B >. <-> y = A )
14 9 13 anbi12ci 
 |-  ( ( x _E y /\ y `' 1st <. A , B >. ) <-> ( y = A /\ x e. y ) )
15 14 exbii 
 |-  ( E. y ( x _E y /\ y `' 1st <. A , B >. ) <-> E. y ( y = A /\ x e. y ) )
16 vex 
 |-  x e. _V
17 16 4 brco 
 |-  ( x ( `' 1st o. _E ) <. A , B >. <-> E. y ( x _E y /\ y `' 1st <. A , B >. ) )
18 1 clel3 
 |-  ( x e. A <-> E. y ( y = A /\ x e. y ) )
19 15 17 18 3bitr4i 
 |-  ( x ( `' 1st o. _E ) <. A , B >. <-> x e. A )
20 10 4 brcnv 
 |-  ( y `' 2nd <. A , B >. <-> <. A , B >. 2nd y )
21 1 2 br2ndeq 
 |-  ( <. A , B >. 2nd y <-> y = B )
22 20 21 bitri 
 |-  ( y `' 2nd <. A , B >. <-> y = B )
23 9 22 anbi12ci 
 |-  ( ( x _E y /\ y `' 2nd <. A , B >. ) <-> ( y = B /\ x e. y ) )
24 23 exbii 
 |-  ( E. y ( x _E y /\ y `' 2nd <. A , B >. ) <-> E. y ( y = B /\ x e. y ) )
25 16 4 brco 
 |-  ( x ( `' 2nd o. _E ) <. A , B >. <-> E. y ( x _E y /\ y `' 2nd <. A , B >. ) )
26 2 clel3 
 |-  ( x e. B <-> E. y ( y = B /\ x e. y ) )
27 24 25 26 3bitr4i 
 |-  ( x ( `' 2nd o. _E ) <. A , B >. <-> x e. B )
28 19 27 anbi12i 
 |-  ( ( x ( `' 1st o. _E ) <. A , B >. /\ x ( `' 2nd o. _E ) <. A , B >. ) <-> ( x e. A /\ x e. B ) )
29 brin 
 |-  ( x ( ( `' 1st o. _E ) i^i ( `' 2nd o. _E ) ) <. A , B >. <-> ( x ( `' 1st o. _E ) <. A , B >. /\ x ( `' 2nd o. _E ) <. A , B >. ) )
30 elin 
 |-  ( x e. ( A i^i B ) <-> ( x e. A /\ x e. B ) )
31 28 29 30 3bitr4ri 
 |-  ( x e. ( A i^i B ) <-> x ( ( `' 1st o. _E ) i^i ( `' 2nd o. _E ) ) <. A , B >. )
32 4 3 5 8 31 brtxpsd3 
 |-  ( <. A , B >. Cap C <-> C = ( A i^i B ) )