Metamath Proof Explorer

Theorem mrelatlub

Description: Least upper bounds in a Moore space are realized by the closure of the union. (Contributed by Stefan O'Rear, 31-Jan-2015) See mrelatlubALT for an alternate proof.

Ref Expression
Hypotheses mreclat.i 
|- I = ( toInc ` C )
mrelatlub.f 
|- F = ( mrCls ` C )
mrelatlub.l 
|- L = ( lub ` I )
Assertion mrelatlub 
|- ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) )

Proof

Step Hyp Ref Expression
1 mreclat.i 
 |-  I = ( toInc ` C )
2 mrelatlub.f 
 |-  F = ( mrCls ` C )
3 mrelatlub.l 
 |-  L = ( lub ` I )
4 eqid 
 |-  ( le ` I ) = ( le ` I )
5 1 ipobas 
 |-  ( C e. ( Moore ` X ) -> C = ( Base ` I ) )
6 5 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> C = ( Base ` I ) )
7 3 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> L = ( lub ` I ) )
8 1 ipopos 
 |-  I e. Poset
9 8 a1i 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> I e. Poset )
10 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U C_ C )
11 uniss 
 |-  ( U C_ C -> U. U C_ U. C )
12 11 adantl 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U. U C_ U. C )
13 mreuni 
 |-  ( C e. ( Moore ` X ) -> U. C = X )
14 13 adantr 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U. C = X )
15 12 14 sseqtrd 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U. U C_ X )
16 2 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ X ) -> ( F ` U. U ) e. C )
17 15 16 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( F ` U. U ) e. C )
18 elssuni 
 |-  ( x e. U -> x C_ U. U )
19 2 mrcssid 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ X ) -> U. U C_ ( F ` U. U ) )
20 15 19 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> U. U C_ ( F ` U. U ) )
21 18 20 sylan9ssr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> x C_ ( F ` U. U ) )
22 simpll 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> C e. ( Moore ` X ) )
23 10 sselda 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> x e. C )
24 17 adantr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> ( F ` U. U ) e. C )
25 1 4 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ x e. C /\ ( F ` U. U ) e. C ) -> ( x ( le ` I ) ( F ` U. U ) <-> x C_ ( F ` U. U ) ) )
26 22 23 24 25 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> ( x ( le ` I ) ( F ` U. U ) <-> x C_ ( F ` U. U ) ) )
27 21 26 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ x e. U ) -> x ( le ` I ) ( F ` U. U ) )
28 simp1l 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> C e. ( Moore ` X ) )
29 simplll 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) /\ x e. U ) -> C e. ( Moore ` X ) )
30 simplr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) -> U C_ C )
31 30 sselda 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) /\ x e. U ) -> x e. C )
32 simplr 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) /\ x e. U ) -> y e. C )
33 1 4 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ x e. C /\ y e. C ) -> ( x ( le ` I ) y <-> x C_ y ) )
34 29 31 32 33 syl3anc 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) /\ x e. U ) -> ( x ( le ` I ) y <-> x C_ y ) )
35 34 biimpd 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) /\ x e. U ) -> ( x ( le ` I ) y -> x C_ y ) )
36 35 ralimdva 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C ) -> ( A. x e. U x ( le ` I ) y -> A. x e. U x C_ y ) )
37 36 3impia 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> A. x e. U x C_ y )
38 unissb 
 |-  ( U. U C_ y <-> A. x e. U x C_ y )
39 37 38 sylibr 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> U. U C_ y )
40 simp2 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> y e. C )
41 2 mrcsscl 
 |-  ( ( C e. ( Moore ` X ) /\ U. U C_ y /\ y e. C ) -> ( F ` U. U ) C_ y )
42 28 39 40 41 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> ( F ` U. U ) C_ y )
43 17 3ad2ant1 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> ( F ` U. U ) e. C )
44 1 4 ipole 
 |-  ( ( C e. ( Moore ` X ) /\ ( F ` U. U ) e. C /\ y e. C ) -> ( ( F ` U. U ) ( le ` I ) y <-> ( F ` U. U ) C_ y ) )
45 28 43 40 44 syl3anc 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> ( ( F ` U. U ) ( le ` I ) y <-> ( F ` U. U ) C_ y ) )
46 42 45 mpbird 
 |-  ( ( ( C e. ( Moore ` X ) /\ U C_ C ) /\ y e. C /\ A. x e. U x ( le ` I ) y ) -> ( F ` U. U ) ( le ` I ) y )
47 4 6 7 9 10 17 27 46 poslubdg 
 |-  ( ( C e. ( Moore ` X ) /\ U C_ C ) -> ( L ` U ) = ( F ` U. U ) )