Metamath Proof Explorer

Theorem mreclat

Description: A Moore space is a complete lattice under inclusion. (Contributed by Zhi Wang, 30-Sep-2024)

Ref Expression
Hypothesis mreclatGOOD.i 
|- I = ( toInc ` C )
Assertion mreclat 
|- ( C e. ( Moore ` X ) -> I e. CLat )

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i 
 |-  I = ( toInc ` C )
2 1 ipobas 
 |-  ( C e. ( Moore ` X ) -> C = ( Base ` I ) )
3 eqidd 
 |-  ( C e. ( Moore ` X ) -> ( lub ` I ) = ( lub ` I ) )
4 eqidd 
 |-  ( C e. ( Moore ` X ) -> ( glb ` I ) = ( glb ` I ) )
5 1 ipopos 
 |-  I e. Poset
6 5 a1i 
 |-  ( C e. ( Moore ` X ) -> I e. Poset )
7 mreuniss 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. x C_ X )
8 eqid 
 |-  ( mrCls ` C ) = ( mrCls ` C )
9 8 mrccl 
 |-  ( ( C e. ( Moore ` X ) /\ U. x C_ X ) -> ( ( mrCls ` C ) ` U. x ) e. C )
10 7 9 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( mrCls ` C ) ` U. x ) e. C )
11 simpl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> C e. ( Moore ` X ) )
12 simpr 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> x C_ C )
13 eqidd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( lub ` I ) = ( lub ` I ) )
14 8 mrcval 
 |-  ( ( C e. ( Moore ` X ) /\ U. x C_ X ) -> ( ( mrCls ` C ) ` U. x ) = |^| { y e. C | U. x C_ y } )
15 7 14 syldan 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( ( mrCls ` C ) ` U. x ) = |^| { y e. C | U. x C_ y } )
16 1 11 12 13 15 ipolubdm 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( x e. dom ( lub ` I ) <-> ( ( mrCls ` C ) ` U. x ) e. C ) )
17 10 16 mpbird 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> x e. dom ( lub ` I ) )
18 ssv 
 |-  y C_ _V
19 int0 
 |-  |^| (/) = _V
20 18 19 sseqtrri 
 |-  y C_ |^| (/)
21 simplr 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) /\ y e. C ) -> x = (/) )
22 21 inteqd 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) /\ y e. C ) -> |^| x = |^| (/) )
23 20 22 sseqtrrid 
 |-  ( ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) /\ y e. C ) -> y C_ |^| x )
24 23 rabeqcda 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> { y e. C | y C_ |^| x } = C )
25 24 unieqd 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> U. { y e. C | y C_ |^| x } = U. C )
26 mreuni 
 |-  ( C e. ( Moore ` X ) -> U. C = X )
27 mre1cl 
 |-  ( C e. ( Moore ` X ) -> X e. C )
28 26 27 eqeltrd 
 |-  ( C e. ( Moore ` X ) -> U. C e. C )
29 28 ad2antrr 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> U. C e. C )
30 25 29 eqeltrd 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x = (/) ) -> U. { y e. C | y C_ |^| x } e. C )
31 mreintcl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> |^| x e. C )
32 unimax 
 |-  ( |^| x e. C -> U. { y e. C | y C_ |^| x } = |^| x )
33 31 32 syl 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> U. { y e. C | y C_ |^| x } = |^| x )
34 33 31 eqeltrd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C /\ x =/= (/) ) -> U. { y e. C | y C_ |^| x } e. C )
35 34 3expa 
 |-  ( ( ( C e. ( Moore ` X ) /\ x C_ C ) /\ x =/= (/) ) -> U. { y e. C | y C_ |^| x } e. C )
36 30 35 pm2.61dane 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. { y e. C | y C_ |^| x } e. C )
37 eqidd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( glb ` I ) = ( glb ` I ) )
38 eqidd 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> U. { y e. C | y C_ |^| x } = U. { y e. C | y C_ |^| x } )
39 1 11 12 37 38 ipoglbdm 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> ( x e. dom ( glb ` I ) <-> U. { y e. C | y C_ |^| x } e. C ) )
40 36 39 mpbird 
 |-  ( ( C e. ( Moore ` X ) /\ x C_ C ) -> x e. dom ( glb ` I ) )
41 2 3 4 6 17 40 isclatd 
 |-  ( C e. ( Moore ` X ) -> I e. CLat )