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 ‘ 𝑋 ) ∧ 𝑈 ⊆ 𝐶 ) → ( 𝐿 ‘ 𝑈 ) = ( 𝐹 ‘ ∪ 𝑈 ) )