Metamath Proof Explorer

Theorem ipolub

Description: The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with S e. dom U .) Could be significantly shortened if poslubdg is in quantified form. mrelatlub could potentially be shortened using this. See mrelatlubALT . (Contributed by Zhi Wang, 28-Sep-2024)

Ref Expression
Hypotheses ipolub.i 
|- I = ( toInc ` F )
ipolub.f 
|- ( ph -> F e. V )
ipolub.s 
|- ( ph -> S C_ F )
ipolub.u 
|- ( ph -> U = ( lub ` I ) )
ipolubdm.t 
|- ( ph -> T = |^| { x e. F | U. S C_ x } )
ipolub.t 
|- ( ph -> T e. F )
Assertion ipolub 
|- ( ph -> ( U ` S ) = T )

Proof

Step Hyp Ref Expression
1 ipolub.i 
 |-  I = ( toInc ` F )
2 ipolub.f 
 |-  ( ph -> F e. V )
3 ipolub.s 
 |-  ( ph -> S C_ F )
4 ipolub.u 
 |-  ( ph -> U = ( lub ` I ) )
5 ipolubdm.t 
 |-  ( ph -> T = |^| { x e. F | U. S C_ x } )
6 ipolub.t 
 |-  ( ph -> T e. F )
7 eqid 
 |-  ( le ` I ) = ( le ` I )
8 1 ipobas 
 |-  ( F e. V -> F = ( Base ` I ) )
9 2 8 syl 
 |-  ( ph -> F = ( Base ` I ) )
10 1 ipopos 
 |-  I e. Poset
11 10 a1i 
 |-  ( ph -> I e. Poset )
12 breq1 
 |-  ( w = y -> ( w ( le ` I ) T <-> y ( le ` I ) T ) )
13 intubeu 
 |-  ( T e. F -> ( ( U. S C_ T /\ A. v e. F ( U. S C_ v -> T C_ v ) ) <-> T = |^| { x e. F | U. S C_ x } ) )
14 13 biimpar 
 |-  ( ( T e. F /\ T = |^| { x e. F | U. S C_ x } ) -> ( U. S C_ T /\ A. v e. F ( U. S C_ v -> T C_ v ) ) )
15 6 5 14 syl2anc 
 |-  ( ph -> ( U. S C_ T /\ A. v e. F ( U. S C_ v -> T C_ v ) ) )
16 1 2 3 7 ipolublem 
 |-  ( ( ph /\ T e. F ) -> ( ( U. S C_ T /\ A. v e. F ( U. S C_ v -> T C_ v ) ) <-> ( A. w e. S w ( le ` I ) T /\ A. v e. F ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) ) ) )
17 6 16 mpdan 
 |-  ( ph -> ( ( U. S C_ T /\ A. v e. F ( U. S C_ v -> T C_ v ) ) <-> ( A. w e. S w ( le ` I ) T /\ A. v e. F ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) ) ) )
18 15 17 mpbid 
 |-  ( ph -> ( A. w e. S w ( le ` I ) T /\ A. v e. F ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) ) )
19 18 simpld 
 |-  ( ph -> A. w e. S w ( le ` I ) T )
20 19 adantr 
 |-  ( ( ph /\ y e. S ) -> A. w e. S w ( le ` I ) T )
21 simpr 
 |-  ( ( ph /\ y e. S ) -> y e. S )
22 12 20 21 rspcdva 
 |-  ( ( ph /\ y e. S ) -> y ( le ` I ) T )
23 breq2 
 |-  ( v = z -> ( w ( le ` I ) v <-> w ( le ` I ) z ) )
24 23 ralbidv 
 |-  ( v = z -> ( A. w e. S w ( le ` I ) v <-> A. w e. S w ( le ` I ) z ) )
25 breq1 
 |-  ( w = y -> ( w ( le ` I ) z <-> y ( le ` I ) z ) )
26 25 cbvralvw 
 |-  ( A. w e. S w ( le ` I ) z <-> A. y e. S y ( le ` I ) z )
27 24 26 bitrdi 
 |-  ( v = z -> ( A. w e. S w ( le ` I ) v <-> A. y e. S y ( le ` I ) z ) )
28 breq2 
 |-  ( v = z -> ( T ( le ` I ) v <-> T ( le ` I ) z ) )
29 27 28 imbi12d 
 |-  ( v = z -> ( ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) <-> ( A. y e. S y ( le ` I ) z -> T ( le ` I ) z ) ) )
30 18 simprd 
 |-  ( ph -> A. v e. F ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) )
31 30 adantr 
 |-  ( ( ph /\ z e. F ) -> A. v e. F ( A. w e. S w ( le ` I ) v -> T ( le ` I ) v ) )
32 simpr 
 |-  ( ( ph /\ z e. F ) -> z e. F )
33 29 31 32 rspcdva 
 |-  ( ( ph /\ z e. F ) -> ( A. y e. S y ( le ` I ) z -> T ( le ` I ) z ) )
34 33 3impia 
 |-  ( ( ph /\ z e. F /\ A. y e. S y ( le ` I ) z ) -> T ( le ` I ) z )
35 7 9 4 11 3 6 22 34 poslubdg 
 |-  ( ph -> ( U ` S ) = T )