Metamath Proof Explorer

Theorem brub

Description: Binary relation form of the upper bound functor. (Contributed by Scott Fenton, 3-May-2018)

Ref Expression
Hypotheses brub.1 
|- S e. _V
brub.2 
|- A e. _V
Assertion brub 
|- ( S UB R A <-> A. x e. S x R A )

Proof

Step Hyp Ref Expression
1 brub.1 
 |-  S e. _V
2 brub.2 
 |-  A e. _V
3 brxp 
 |-  ( S ( _V X. _V ) A <-> ( S e. _V /\ A e. _V ) )
4 1 2 3 mpbir2an 
 |-  S ( _V X. _V ) A
5 brdif 
 |-  ( S ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) ) A <-> ( S ( _V X. _V ) A /\ -. S ( ( _V \ R ) o. `' _E ) A ) )
6 4 5 mpbiran 
 |-  ( S ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) ) A <-> -. S ( ( _V \ R ) o. `' _E ) A )
7 1 2 coepr 
 |-  ( S ( ( _V \ R ) o. `' _E ) A <-> E. x e. S x ( _V \ R ) A )
8 6 7 xchbinx 
 |-  ( S ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) ) A <-> -. E. x e. S x ( _V \ R ) A )
9 df-ub 
 |-  UB R = ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) )
10 9 breqi 
 |-  ( S UB R A <-> S ( ( _V X. _V ) \ ( ( _V \ R ) o. `' _E ) ) A )
11 brv 
 |-  x _V A
12 brdif 
 |-  ( x ( _V \ R ) A <-> ( x _V A /\ -. x R A ) )
13 11 12 mpbiran 
 |-  ( x ( _V \ R ) A <-> -. x R A )
14 13 rexbii 
 |-  ( E. x e. S x ( _V \ R ) A <-> E. x e. S -. x R A )
15 rexnal 
 |-  ( E. x e. S -. x R A <-> -. A. x e. S x R A )
16 14 15 bitri 
 |-  ( E. x e. S x ( _V \ R ) A <-> -. A. x e. S x R A )
17 16 con2bii 
 |-  ( A. x e. S x R A <-> -. E. x e. S x ( _V \ R ) A )
18 8 10 17 3bitr4i 
 |-  ( S UB R A <-> A. x e. S x R A )