Metamath Proof Explorer

Theorem brcup

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

Ref Expression
Hypotheses brcup.1 
|- A e. _V
brcup.2 
|- B e. _V
brcup.3 
|- C e. _V
Assertion brcup 
|- ( <. A , B >. Cup C <-> C = ( A u. B ) )

Proof

Step Hyp Ref Expression
1 brcup.1 
 |-  A e. _V
2 brcup.2 
 |-  B e. _V
3 brcup.3 
 |-  C e. _V
4 opex 
 |-  <. A , B >. e. _V
5 df-cup 
 |-  Cup = ( ( ( _V X. _V ) X. _V ) \ ran ( ( _V (x) _E ) /_\ ( ( ( `' 1st o. _E ) u. ( `' 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 orbi12i 
 |-  ( ( x ( `' 1st o. _E ) <. A , B >. \/ x ( `' 2nd o. _E ) <. A , B >. ) <-> ( x e. A \/ x e. B ) )
29 brun 
 |-  ( x ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) <. A , B >. <-> ( x ( `' 1st o. _E ) <. A , B >. \/ x ( `' 2nd o. _E ) <. A , B >. ) )
30 elun 
 |-  ( x e. ( A u. B ) <-> ( x e. A \/ x e. B ) )
31 28 29 30 3bitr4ri 
 |-  ( x e. ( A u. B ) <-> x ( ( `' 1st o. _E ) u. ( `' 2nd o. _E ) ) <. A , B >. )
32 4 3 5 8 31 brtxpsd3 
 |-  ( <. A , B >. Cup C <-> C = ( A u. B ) )