Theorem toslub

Description: In a toset, the lowest upper bound lub , defined for partial orders is the supremum, sup ( A , B , .< ) , defined for total orders. (these are the set.mm definitions: lowest upper bound and supremum are normally synonymous). Note that those two values are also equal if such a supremum does not exist: in that case, both are equal to the empty set. (Contributed by Thierry Arnoux, 15-Feb-2018) (Revised by Thierry Arnoux, 24-Sep-2018)

	Ref	Expression
Hypotheses	toslub.b	|- B = ( Base ` K )
	toslub.l	|- .< = ( lt ` K )
	toslub.1	|- ( ph -> K e. Toset )
	toslub.2	|- ( ph -> A C_ B )
Assertion	toslub	|- ( ph -> ( ( lub ` K ) ` A ) = sup ( A , B , .< ) )

Proof

Step	Hyp	Ref	Expression
1		toslub.b	|- B = ( Base ` K )
2		toslub.l	|- .< = ( lt ` K )
3		toslub.1	|- ( ph -> K e. Toset )
4		toslub.2	|- ( ph -> A C_ B )
5		eqid	|- ( le ` K ) = ( le ` K )
6	1 2 3 4 5	toslublem	|- ( ( ph /\ a e. B ) -> ( ( A. b e. A b ( le ` K ) a /\ A. c e. B ( A. b e. A b ( le ` K ) c -> a ( le ` K ) c ) ) <-> ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )
7	6	riotabidva	|- ( ph -> ( iota_ a e. B ( A. b e. A b ( le ` K ) a /\ A. c e. B ( A. b e. A b ( le ` K ) c -> a ( le ` K ) c ) ) ) = ( iota_ a e. B ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )
8		eqid	|- ( lub ` K ) = ( lub ` K )
9		biid	|- ( ( A. b e. A b ( le ` K ) a /\ A. c e. B ( A. b e. A b ( le ` K ) c -> a ( le ` K ) c ) ) <-> ( A. b e. A b ( le ` K ) a /\ A. c e. B ( A. b e. A b ( le ` K ) c -> a ( le ` K ) c ) ) )
10	1 5 8 9 3 4	lubval	|- ( ph -> ( ( lub ` K ) ` A ) = ( iota_ a e. B ( A. b e. A b ( le ` K ) a /\ A. c e. B ( A. b e. A b ( le ` K ) c -> a ( le ` K ) c ) ) ) )
11	1 5 2	tosso	|- ( K e. Toset -> ( K e. Toset <-> ( .< Or B /\ ( _I |` B ) C_ ( le ` K ) ) ) )
12	11	ibi	|- ( K e. Toset -> ( .< Or B /\ ( _I |` B ) C_ ( le ` K ) ) )
13	12	simpld	|- ( K e. Toset -> .< Or B )
14		id	|- ( .< Or B -> .< Or B )
15	14	supval2	|- ( .< Or B -> sup ( A , B , .< ) = ( iota_ a e. B ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )
16	3 13 15	3syl	|- ( ph -> sup ( A , B , .< ) = ( iota_ a e. B ( A. b e. A -. a .< b /\ A. b e. B ( b .< a -> E. d e. A b .< d ) ) ) )
17	7 10 16	3eqtr4d	|- ( ph -> ( ( lub ` K ) ` A ) = sup ( A , B , .< ) )