This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐼 = ( toInc ‘ 𝐶 )
Assertion mreclat ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ CLat )

Proof

Step Hyp Ref Expression
1 mreclatGOOD.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
2 1 ipobas ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = ( Base ‘ 𝐼 ) )
3 eqidd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
4 eqidd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 ) )
5 1 ipopos ⊢ 𝐼 ∈ Poset
6 5 a1i ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ Poset )
7 mreuniss ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ 𝑥 ⊆ 𝑋 )
8 eqid ⊢ ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 )
9 8 mrccl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑥 ⊆ 𝑋 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) ∈ 𝐶 )
10 7 9 syldan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) ∈ 𝐶 )
11 simpl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
12 simpr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → 𝑥 ⊆ 𝐶 )
13 eqidd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 ) )
14 8 mrcval ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑥 ⊆ 𝑋 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) = ∩ { 𝑦 ∈ 𝐶 ∣ ∪ 𝑥 ⊆ 𝑦 } )
15 7 14 syldan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) = ∩ { 𝑦 ∈ 𝐶 ∣ ∪ 𝑥 ⊆ 𝑦 } )
16 1 11 12 13 15 ipolubdm ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( 𝑥 ∈ dom ( lub ‘ 𝐼 ) ↔ ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) ∈ 𝐶 ) )
17 10 16 mpbird ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → 𝑥 ∈ dom ( lub ‘ 𝐼 ) )
18 ssv ⊢ 𝑦 ⊆ V
19 int0 ⊢ ∩ ∅ = V
20 18 19 sseqtrri ⊢ 𝑦 ⊆ ∩ ∅
21 simplr ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) ∧ 𝑦 ∈ 𝐶 ) → 𝑥 = ∅ )
22 21 inteqd ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) ∧ 𝑦 ∈ 𝐶 ) → ∩ 𝑥 = ∩ ∅ )
23 20 22 sseqtrrid ⊢ ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) ∧ 𝑦 ∈ 𝐶 ) → 𝑦 ⊆ ∩ 𝑥 )
24 23 rabeqcda ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } = 𝐶 )
25 24 unieqd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } = ∪ 𝐶 )
26 mreuni ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )
27 mre1cl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
28 26 27 eqeltrd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 ∈ 𝐶 )
29 28 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ∪ 𝐶 ∈ 𝐶 )
30 25 29 eqeltrd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐶 )
31 mreintcl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐶 )
32 unimax ⊢ ( ∩ 𝑥 ∈ 𝐶 → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } = ∩ 𝑥 )
33 31 32 syl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } = ∩ 𝑥 )
34 33 31 eqeltrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐶 )
35 34 3expa ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 ≠ ∅ ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐶 )
36 30 35 pm2.61dane ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐶 )
37 eqidd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 ) )
38 eqidd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } = ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } )
39 1 11 12 37 38 ipoglbdm ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( 𝑥 ∈ dom ( glb ‘ 𝐼 ) ↔ ∪ { 𝑦 ∈ 𝐶 ∣ 𝑦 ⊆ ∩ 𝑥 } ∈ 𝐶 ) )
40 36 39 mpbird ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → 𝑥 ∈ dom ( glb ‘ 𝐼 ) )
41 2 3 4 6 17 40 isclatd ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ CLat )