Metamath Proof Explorer

Theorem lubsscl

Description: If a subset of S contains the LUB of S , then the two sets have the same LUB. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubsscl.k 
|- ( ph -> K e. Poset )
lubsscl.t 
|- ( ph -> T C_ S )
lubsscl.u 
|- U = ( lub ` K )
lubsscl.s 
|- ( ph -> S e. dom U )
lubsscl.x 
|- ( ph -> ( U ` S ) e. T )
Assertion lubsscl 
|- ( ph -> ( T e. dom U /\ ( U ` T ) = ( U ` S ) ) )

Proof

Step Hyp Ref Expression
1 lubsscl.k 
 |-  ( ph -> K e. Poset )
2 lubsscl.t 
 |-  ( ph -> T C_ S )
3 lubsscl.u 
 |-  U = ( lub ` K )
4 lubsscl.s 
 |-  ( ph -> S e. dom U )
5 lubsscl.x 
 |-  ( ph -> ( U ` S ) e. T )
6 eqid 
 |-  ( Base ` K ) = ( Base ` K )
7 eqid 
 |-  ( le ` K ) = ( le ` K )
8 6 7 3 1 4 lubelss 
 |-  ( ph -> S C_ ( Base ` K ) )
9 2 8 sstrd 
 |-  ( ph -> T C_ ( Base ` K ) )
10 9 5 sseldd 
 |-  ( ph -> ( U ` S ) e. ( Base ` K ) )
11 1 adantr 
 |-  ( ( ph /\ y e. T ) -> K e. Poset )
12 4 adantr 
 |-  ( ( ph /\ y e. T ) -> S e. dom U )
13 2 sselda 
 |-  ( ( ph /\ y e. T ) -> y e. S )
14 6 7 3 11 12 13 luble 
 |-  ( ( ph /\ y e. T ) -> y ( le ` K ) ( U ` S ) )
15 14 ralrimiva 
 |-  ( ph -> A. y e. T y ( le ` K ) ( U ` S ) )
16 breq1 
 |-  ( y = ( U ` S ) -> ( y ( le ` K ) z <-> ( U ` S ) ( le ` K ) z ) )
17 simp3 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T y ( le ` K ) z ) -> A. y e. T y ( le ` K ) z )
18 5 3ad2ant1 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T y ( le ` K ) z ) -> ( U ` S ) e. T )
19 16 17 18 rspcdva 
 |-  ( ( ph /\ z e. ( Base ` K ) /\ A. y e. T y ( le ` K ) z ) -> ( U ` S ) ( le ` K ) z )
20 19 3expia 
 |-  ( ( ph /\ z e. ( Base ` K ) ) -> ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) )
21 20 ralrimiva 
 |-  ( ph -> A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) )
22 breq2 
 |-  ( x = ( U ` S ) -> ( y ( le ` K ) x <-> y ( le ` K ) ( U ` S ) ) )
23 22 ralbidv 
 |-  ( x = ( U ` S ) -> ( A. y e. T y ( le ` K ) x <-> A. y e. T y ( le ` K ) ( U ` S ) ) )
24 breq1 
 |-  ( x = ( U ` S ) -> ( x ( le ` K ) z <-> ( U ` S ) ( le ` K ) z ) )
25 24 imbi2d 
 |-  ( x = ( U ` S ) -> ( ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) <-> ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) ) )
26 25 ralbidv 
 |-  ( x = ( U ` S ) -> ( A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) <-> A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) ) )
27 23 26 anbi12d 
 |-  ( x = ( U ` S ) -> ( ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) <-> ( A. y e. T y ( le ` K ) ( U ` S ) /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) ) ) )
28 27 rspcev 
 |-  ( ( ( U ` S ) e. ( Base ` K ) /\ ( A. y e. T y ( le ` K ) ( U ` S ) /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> ( U ` S ) ( le ` K ) z ) ) ) -> E. x e. ( Base ` K ) ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) )
29 10 15 21 28 syl12anc 
 |-  ( ph -> E. x e. ( Base ` K ) ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) )
30 biid 
 |-  ( ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) <-> ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) )
31 6 7 3 30 1 lubeldm2 
 |-  ( ph -> ( T e. dom U <-> ( T C_ ( Base ` K ) /\ E. x e. ( Base ` K ) ( A. y e. T y ( le ` K ) x /\ A. z e. ( Base ` K ) ( A. y e. T y ( le ` K ) z -> x ( le ` K ) z ) ) ) ) )
32 9 29 31 mpbir2and 
 |-  ( ph -> T e. dom U )
33 7 6 3 1 9 10 14 19 poslubd 
 |-  ( ph -> ( U ` T ) = ( U ` S ) )
34 32 33 jca 
 |-  ( ph -> ( T e. dom U /\ ( U ` T ) = ( U ` S ) ) )