Metamath Proof Explorer

Theorem dfsup2

Description: Quantifier-free definition of supremum. (Contributed by Scott Fenton, 19-Feb-2013)

Ref Expression
Assertion dfsup2 
|- sup ( B , A , R ) = U. ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )

Proof

Step Hyp Ref Expression
1 df-sup 
 |-  sup ( B , A , R ) = U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) }
2 dfrab3 
 |-  { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = ( A i^i { x | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
3 abeq1 
 |-  ( { x | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) <-> A. x ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) <-> x e. ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) ) )
4 vex 
 |-  x e. _V
5 eldif 
 |-  ( x e. ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) <-> ( x e. _V /\ -. x e. ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) )
6 4 5 mpbiran 
 |-  ( x e. ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) <-> -. x e. ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
7 4 elima 
 |-  ( x e. ( `' R " B ) <-> E. y e. B y `' R x )
8 dfrex2 
 |-  ( E. y e. B y `' R x <-> -. A. y e. B -. y `' R x )
9 7 8 bitri 
 |-  ( x e. ( `' R " B ) <-> -. A. y e. B -. y `' R x )
10 4 elima 
 |-  ( x e. ( R " ( A \ ( `' R " B ) ) ) <-> E. y e. ( A \ ( `' R " B ) ) y R x )
11 dfrex2 
 |-  ( E. y e. ( A \ ( `' R " B ) ) y R x <-> -. A. y e. ( A \ ( `' R " B ) ) -. y R x )
12 10 11 bitri 
 |-  ( x e. ( R " ( A \ ( `' R " B ) ) ) <-> -. A. y e. ( A \ ( `' R " B ) ) -. y R x )
13 9 12 orbi12i 
 |-  ( ( x e. ( `' R " B ) \/ x e. ( R " ( A \ ( `' R " B ) ) ) ) <-> ( -. A. y e. B -. y `' R x \/ -. A. y e. ( A \ ( `' R " B ) ) -. y R x ) )
14 elun 
 |-  ( x e. ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) <-> ( x e. ( `' R " B ) \/ x e. ( R " ( A \ ( `' R " B ) ) ) ) )
15 ianor 
 |-  ( -. ( A. y e. B -. y `' R x /\ A. y e. ( A \ ( `' R " B ) ) -. y R x ) <-> ( -. A. y e. B -. y `' R x \/ -. A. y e. ( A \ ( `' R " B ) ) -. y R x ) )
16 13 14 15 3bitr4i 
 |-  ( x e. ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) <-> -. ( A. y e. B -. y `' R x /\ A. y e. ( A \ ( `' R " B ) ) -. y R x ) )
17 16 con2bii 
 |-  ( ( A. y e. B -. y `' R x /\ A. y e. ( A \ ( `' R " B ) ) -. y R x ) <-> -. x e. ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
18 vex 
 |-  y e. _V
19 18 4 brcnv 
 |-  ( y `' R x <-> x R y )
20 19 notbii 
 |-  ( -. y `' R x <-> -. x R y )
21 20 ralbii 
 |-  ( A. y e. B -. y `' R x <-> A. y e. B -. x R y )
22 impexp 
 |-  ( ( ( y e. A /\ -. y e. ( `' R " B ) ) -> -. y R x ) <-> ( y e. A -> ( -. y e. ( `' R " B ) -> -. y R x ) ) )
23 eldif 
 |-  ( y e. ( A \ ( `' R " B ) ) <-> ( y e. A /\ -. y e. ( `' R " B ) ) )
24 23 imbi1i 
 |-  ( ( y e. ( A \ ( `' R " B ) ) -> -. y R x ) <-> ( ( y e. A /\ -. y e. ( `' R " B ) ) -> -. y R x ) )
25 18 elima 
 |-  ( y e. ( `' R " B ) <-> E. z e. B z `' R y )
26 vex 
 |-  z e. _V
27 26 18 brcnv 
 |-  ( z `' R y <-> y R z )
28 27 rexbii 
 |-  ( E. z e. B z `' R y <-> E. z e. B y R z )
29 25 28 bitri 
 |-  ( y e. ( `' R " B ) <-> E. z e. B y R z )
30 29 imbi2i 
 |-  ( ( y R x -> y e. ( `' R " B ) ) <-> ( y R x -> E. z e. B y R z ) )
31 con34b 
 |-  ( ( y R x -> y e. ( `' R " B ) ) <-> ( -. y e. ( `' R " B ) -> -. y R x ) )
32 30 31 bitr3i 
 |-  ( ( y R x -> E. z e. B y R z ) <-> ( -. y e. ( `' R " B ) -> -. y R x ) )
33 32 imbi2i 
 |-  ( ( y e. A -> ( y R x -> E. z e. B y R z ) ) <-> ( y e. A -> ( -. y e. ( `' R " B ) -> -. y R x ) ) )
34 22 24 33 3bitr4i 
 |-  ( ( y e. ( A \ ( `' R " B ) ) -> -. y R x ) <-> ( y e. A -> ( y R x -> E. z e. B y R z ) ) )
35 34 ralbii2 
 |-  ( A. y e. ( A \ ( `' R " B ) ) -. y R x <-> A. y e. A ( y R x -> E. z e. B y R z ) )
36 21 35 anbi12i 
 |-  ( ( A. y e. B -. y `' R x /\ A. y e. ( A \ ( `' R " B ) ) -. y R x ) <-> ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
37 6 17 36 3bitr2ri 
 |-  ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) <-> x e. ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) )
38 3 37 mpgbir 
 |-  { x | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
39 38 ineq2i 
 |-  ( A i^i { x | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } ) = ( A i^i ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) )
40 invdif 
 |-  ( A i^i ( _V \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) ) ) = ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
41 39 40 eqtri 
 |-  ( A i^i { x | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } ) = ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
42 2 41 eqtri 
 |-  { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
43 42 unieqi 
 |-  U. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } = U. ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )
44 1 43 eqtri 
 |-  sup ( B , A , R ) = U. ( A \ ( ( `' R " B ) u. ( R " ( A \ ( `' R " B ) ) ) ) )