Metamath Proof Explorer

Theorem mreclatBAD

Description: A Moore space is a complete lattice under inclusion. (Contributed by Stefan O'Rear, 31-Jan-2015) TODO ( df-riota update): Reprove using isclat instead of the isclatBAD. hypothesis. See commented-out mreclat above. See mreclat for a good version.

Ref Expression
Hypotheses mreclat.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
isclatBAD. ⊢ ( 𝐼 ∈ CLat ↔ ( 𝐼 ∈ Poset ∧ ∀ 𝑥 ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) ) )
Assertion mreclatBAD ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ CLat )

Proof

Step Hyp Ref Expression
1 mreclat.i ⊢ 𝐼 = ( toInc ‘ 𝐶 )
2 isclatBAD. ⊢ ( 𝐼 ∈ CLat ↔ ( 𝐼 ∈ Poset ∧ ∀ 𝑥 ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) ) )
3 1 ipopos ⊢ 𝐼 ∈ Poset
4 3 a1i ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ Poset )
5 eqid ⊢ ( mrCls ‘ 𝐶 ) = ( mrCls ‘ 𝐶 )
6 eqid ⊢ ( lub ‘ 𝐼 ) = ( lub ‘ 𝐼 )
7 1 5 6 mrelatlub ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) = ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) )
8 uniss ⊢ ( 𝑥 ⊆ 𝐶 → ∪ 𝑥 ⊆ ∪ 𝐶 )
9 8 adantl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ 𝑥 ⊆ ∪ 𝐶 )
10 mreuni ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∪ 𝐶 = 𝑋 )
11 10 adantr ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ 𝐶 = 𝑋 )
12 9 11 sseqtrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ∪ 𝑥 ⊆ 𝑋 )
13 5 mrccl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ∪ 𝑥 ⊆ 𝑋 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) ∈ 𝐶 )
14 12 13 syldan ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( mrCls ‘ 𝐶 ) ‘ ∪ 𝑥 ) ∈ 𝐶 )
15 7 14 eqeltrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 )
16 fveq2 ⊢ ( 𝑥 = ∅ → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) = ( ( glb ‘ 𝐼 ) ‘ ∅ ) )
17 16 adantl ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) = ( ( glb ‘ 𝐼 ) ‘ ∅ ) )
18 eqid ⊢ ( glb ‘ 𝐼 ) = ( glb ‘ 𝐼 )
19 1 18 mrelatglb0 ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ( glb ‘ 𝐼 ) ‘ ∅ ) = 𝑋 )
20 19 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ( ( glb ‘ 𝐼 ) ‘ ∅ ) = 𝑋 )
21 17 20 eqtrd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) = 𝑋 )
22 mre1cl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝑋 ∈ 𝐶 )
23 22 ad2antrr ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → 𝑋 ∈ 𝐶 )
24 21 23 eqeltrd ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 = ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 )
25 1 18 mrelatglb ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) = ∩ 𝑥 )
26 mreintcl ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ∩ 𝑥 ∈ 𝐶 )
27 25 26 eqeltrd ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ∧ 𝑥 ≠ ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 )
28 27 3expa ⊢ ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) ∧ 𝑥 ≠ ∅ ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 )
29 24 28 pm2.61dane ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 )
30 15 29 jca ⊢ ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥 ⊆ 𝐶 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ) )
31 30 ex ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑥 ⊆ 𝐶 → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ) ) )
32 1 ipobas ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = ( Base ‘ 𝐼 ) )
33 sseq2 ⊢ ( 𝐶 = ( Base ‘ 𝐼 ) → ( 𝑥 ⊆ 𝐶 ↔ 𝑥 ⊆ ( Base ‘ 𝐼 ) ) )
34 eleq2 ⊢ ( 𝐶 = ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) )
35 eleq2 ⊢ ( 𝐶 = ( Base ‘ 𝐼 ) → ( ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ↔ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) )
36 34 35 anbi12d ⊢ ( 𝐶 = ( Base ‘ 𝐼 ) → ( ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ) ↔ ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) )
37 33 36 imbi12d ⊢ ( 𝐶 = ( Base ‘ 𝐼 ) → ( ( 𝑥 ⊆ 𝐶 → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) ) )
38 32 37 syl ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( ( 𝑥 ⊆ 𝐶 → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ 𝐶 ) ) ↔ ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) ) )
39 31 38 mpbid ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) )
40 39 alrimiv ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → ∀ 𝑥 ( 𝑥 ⊆ ( Base ‘ 𝐼 ) → ( ( ( lub ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ∧ ( ( glb ‘ 𝐼 ) ‘ 𝑥 ) ∈ ( Base ‘ 𝐼 ) ) ) )
41 4 40 2 sylanbrc ⊢ ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐼 ∈ CLat )