Theorem supub

Description: A supremum is an upper bound. See also supcl and suplub .

This proof demonstrates how to expand an iota-based definition ( df-iota ) using riotacl2 .

(Contributed by NM, 12-Oct-2004) (Proof shortened by Mario Carneiro, 24-Dec-2016)

	Ref	Expression
Hypotheses	supmo.1	|- ( ph -> R Or A )
	supcl.2	|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
Assertion	supub	|- ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) )

Proof

Step	Hyp	Ref	Expression
1		supmo.1	|- ( ph -> R Or A )
2		supcl.2	|- ( ph -> E. x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
3		simpl	|- ( ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> A. y e. B -. x R y )
4	3	a1i	|- ( 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. y e. B -. x R y ) )
5	4	ss2rabi	|- { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } C_ { x e. A | A. y e. B -. x R y }
6	1	supval2	|- ( ph -> sup ( B , A , R ) = ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) )
7	1 2	supeu	|- ( ph -> E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) )
8		riotacl2	|- ( E! x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
9	7 8	syl	|- ( ph -> ( iota_ x e. A ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
10	6 9	eqeltrd	|- ( ph -> sup ( B , A , R ) e. { x e. A | ( A. y e. B -. x R y /\ A. y e. A ( y R x -> E. z e. B y R z ) ) } )
11	5 10	sselid	|- ( ph -> sup ( B , A , R ) e. { x e. A | A. y e. B -. x R y } )
12		breq2	|- ( y = w -> ( x R y <-> x R w ) )
13	12	notbid	|- ( y = w -> ( -. x R y <-> -. x R w ) )
14	13	cbvralvw	|- ( A. y e. B -. x R y <-> A. w e. B -. x R w )
15		breq1	|- ( x = sup ( B , A , R ) -> ( x R w <-> sup ( B , A , R ) R w ) )
16	15	notbid	|- ( x = sup ( B , A , R ) -> ( -. x R w <-> -. sup ( B , A , R ) R w ) )
17	16	ralbidv	|- ( x = sup ( B , A , R ) -> ( A. w e. B -. x R w <-> A. w e. B -. sup ( B , A , R ) R w ) )
18	14 17	bitrid	|- ( x = sup ( B , A , R ) -> ( A. y e. B -. x R y <-> A. w e. B -. sup ( B , A , R ) R w ) )
19	18	elrab	|- ( sup ( B , A , R ) e. { x e. A | A. y e. B -. x R y } <-> ( sup ( B , A , R ) e. A /\ A. w e. B -. sup ( B , A , R ) R w ) )
20	19	simprbi	|- ( sup ( B , A , R ) e. { x e. A | A. y e. B -. x R y } -> A. w e. B -. sup ( B , A , R ) R w )
21	11 20	syl	|- ( ph -> A. w e. B -. sup ( B , A , R ) R w )
22		breq2	|- ( w = C -> ( sup ( B , A , R ) R w <-> sup ( B , A , R ) R C ) )
23	22	notbid	|- ( w = C -> ( -. sup ( B , A , R ) R w <-> -. sup ( B , A , R ) R C ) )
24	23	rspccv	|- ( A. w e. B -. sup ( B , A , R ) R w -> ( C e. B -> -. sup ( B , A , R ) R C ) )
25	21 24	syl	|- ( ph -> ( C e. B -> -. sup ( B , A , R ) R C ) )