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 )