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 𝐼 = ( toInc ‘ 𝐶 )
mrelatlub.f 𝐹 = ( mrCls ‘ 𝐶 )
mrelatlub.l 𝐿 = ( lub ‘ 𝐼 )
Assertion mrelatlub ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → ( 𝐿𝑈 ) = ( 𝐹 𝑈 ) )

Proof

Step Hyp Ref Expression
1 mreclat.i 𝐼 = ( toInc ‘ 𝐶 )
2 mrelatlub.f 𝐹 = ( mrCls ‘ 𝐶 )
3 mrelatlub.l 𝐿 = ( lub ‘ 𝐼 )
4 eqid ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
5 1 ipobas ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = ( Base ‘ 𝐼 ) )
6 5 adantr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝐶 = ( Base ‘ 𝐼 ) )
7 3 a1i ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝐿 = ( lub ‘ 𝐼 ) )
8 1 ipopos 𝐼 ∈ Poset
9 8 a1i ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝐼 ∈ Poset )
10 simpr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝑈𝐶 )
11 uniss ( 𝑈𝐶 𝑈 𝐶 )
12 11 adantl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝑈 𝐶 )
13 mreuni ( 𝐶 ∈ ( Moore ‘ 𝑋 ) → 𝐶 = 𝑋 )
14 13 adantr ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝐶 = 𝑋 )
15 12 14 sseqtrd ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝑈𝑋 )
16 2 mrccl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝑋 ) → ( 𝐹 𝑈 ) ∈ 𝐶 )
17 15 16 syldan ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → ( 𝐹 𝑈 ) ∈ 𝐶 )
18 elssuni ( 𝑥𝑈𝑥 𝑈 )
19 2 mrcssid ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝑋 ) → 𝑈 ⊆ ( 𝐹 𝑈 ) )
20 15 19 syldan ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → 𝑈 ⊆ ( 𝐹 𝑈 ) )
21 18 20 sylan9ssr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → 𝑥 ⊆ ( 𝐹 𝑈 ) )
22 simpll ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
23 10 sselda ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → 𝑥𝐶 )
24 17 adantr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → ( 𝐹 𝑈 ) ∈ 𝐶 )
25 1 4 ipole ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥𝐶 ∧ ( 𝐹 𝑈 ) ∈ 𝐶 ) → ( 𝑥 ( le ‘ 𝐼 ) ( 𝐹 𝑈 ) ↔ 𝑥 ⊆ ( 𝐹 𝑈 ) ) )
26 22 23 24 25 syl3anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → ( 𝑥 ( le ‘ 𝐼 ) ( 𝐹 𝑈 ) ↔ 𝑥 ⊆ ( 𝐹 𝑈 ) ) )
27 21 26 mpbird ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑥𝑈 ) → 𝑥 ( le ‘ 𝐼 ) ( 𝐹 𝑈 ) )
28 simp1l ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
29 simplll ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) ∧ 𝑥𝑈 ) → 𝐶 ∈ ( Moore ‘ 𝑋 ) )
30 simplr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) → 𝑈𝐶 )
31 30 sselda ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) ∧ 𝑥𝑈 ) → 𝑥𝐶 )
32 simplr ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) ∧ 𝑥𝑈 ) → 𝑦𝐶 )
33 1 4 ipole ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑥𝐶𝑦𝐶 ) → ( 𝑥 ( le ‘ 𝐼 ) 𝑦𝑥𝑦 ) )
34 29 31 32 33 syl3anc ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) ∧ 𝑥𝑈 ) → ( 𝑥 ( le ‘ 𝐼 ) 𝑦𝑥𝑦 ) )
35 34 biimpd ( ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) ∧ 𝑥𝑈 ) → ( 𝑥 ( le ‘ 𝐼 ) 𝑦𝑥𝑦 ) )
36 35 ralimdva ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ) → ( ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 → ∀ 𝑥𝑈 𝑥𝑦 ) )
37 36 3impia ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → ∀ 𝑥𝑈 𝑥𝑦 )
38 unissb ( 𝑈𝑦 ↔ ∀ 𝑥𝑈 𝑥𝑦 )
39 37 38 sylibr ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → 𝑈𝑦 )
40 simp2 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → 𝑦𝐶 )
41 2 mrcsscl ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝑦𝑦𝐶 ) → ( 𝐹 𝑈 ) ⊆ 𝑦 )
42 28 39 40 41 syl3anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → ( 𝐹 𝑈 ) ⊆ 𝑦 )
43 17 3ad2ant1 ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → ( 𝐹 𝑈 ) ∈ 𝐶 )
44 1 4 ipole ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ ( 𝐹 𝑈 ) ∈ 𝐶𝑦𝐶 ) → ( ( 𝐹 𝑈 ) ( le ‘ 𝐼 ) 𝑦 ↔ ( 𝐹 𝑈 ) ⊆ 𝑦 ) )
45 28 43 40 44 syl3anc ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → ( ( 𝐹 𝑈 ) ( le ‘ 𝐼 ) 𝑦 ↔ ( 𝐹 𝑈 ) ⊆ 𝑦 ) )
46 42 45 mpbird ( ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) ∧ 𝑦𝐶 ∧ ∀ 𝑥𝑈 𝑥 ( le ‘ 𝐼 ) 𝑦 ) → ( 𝐹 𝑈 ) ( le ‘ 𝐼 ) 𝑦 )
47 4 6 7 9 10 17 27 46 poslubdg ( ( 𝐶 ∈ ( Moore ‘ 𝑋 ) ∧ 𝑈𝐶 ) → ( 𝐿𝑈 ) = ( 𝐹 𝑈 ) )