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

Metamath Proof Explorer

Theorem glbsscl

Description: If a subset of S contains the GLB of S , then the two sets have the same GLB. (Contributed by Zhi Wang, 26-Sep-2024)

Ref Expression
Hypotheses lubsscl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lubsscl.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
glbsscl.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
glbsscl.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 )
glbsscl.x ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ 𝑇 )
Assertion glbsscl ( 𝜑 → ( 𝑇 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑇 ) = ( 𝐺 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 lubsscl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
2 lubsscl.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
3 glbsscl.g ⊢ 𝐺 = ( glb ‘ 𝐾 )
4 glbsscl.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝐺 )
5 glbsscl.x ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ 𝑇 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 6 7 3 1 4 glbelss ⊢ ( 𝜑 → 𝑆 ⊆ ( Base ‘ 𝐾 ) )
9 2 8 sstrd ⊢ ( 𝜑 → 𝑇 ⊆ ( Base ‘ 𝐾 ) )
10 9 5 sseldd ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) )
11 1 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝐾 ∈ Poset )
12 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝑆 ∈ dom 𝐺 )
13 2 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ∈ 𝑆 )
14 6 7 3 11 12 13 glble ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 )
16 breq2 ⊢ ( 𝑦 = ( 𝐺 ‘ 𝑆 ) → ( 𝑧 ( le ‘ 𝐾 ) 𝑦 ↔ 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) )
17 simp3 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 ) → ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 )
18 5 3ad2ant1 ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 ) → ( 𝐺 ‘ 𝑆 ) ∈ 𝑇 )
19 16 17 18 rspcdva ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ∧ ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 ) → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) )
20 19 3expia ⊢ ( ( 𝜑 ∧ 𝑧 ∈ ( Base ‘ 𝐾 ) ) → ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) )
21 20 ralrimiva ⊢ ( 𝜑 → ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) )
22 breq1 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 ) )
23 22 ralbidv ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ↔ ∀ 𝑦 ∈ 𝑇 ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 ) )
24 breq2 ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( 𝑧 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) )
25 24 imbi2d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ↔ ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) )
26 25 ralbidv ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ↔ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) )
27 23 26 anbi12d ⊢ ( 𝑥 = ( 𝐺 ‘ 𝑆 ) → ( ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑇 ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) ) )
28 27 rspcev ⊢ ( ( ( 𝐺 ‘ 𝑆 ) ∈ ( Base ‘ 𝐾 ) ∧ ( ∀ 𝑦 ∈ 𝑇 ( 𝐺 ‘ 𝑆 ) ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) ( 𝐺 ‘ 𝑆 ) ) ) ) → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
29 10 15 21 28 syl12anc ⊢ ( 𝜑 → ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
30 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ↔ ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) )
31 6 7 3 30 1 glbeldm2 ⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝐺 ↔ ( 𝑇 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑥 ( le ‘ 𝐾 ) 𝑦 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑧 ( le ‘ 𝐾 ) 𝑦 → 𝑧 ( le ‘ 𝐾 ) 𝑥 ) ) ) ) )
32 9 29 31 mpbir2and ⊢ ( 𝜑 → 𝑇 ∈ dom 𝐺 )
33 eqidd ⊢ ( 𝜑 → ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 ) )
34 3 a1i ⊢ ( 𝜑 → 𝐺 = ( glb ‘ 𝐾 ) )
35 7 33 34 1 9 10 14 19 posglbdg ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑇 ) = ( 𝐺 ‘ 𝑆 ) )
36 32 35 jca ⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑇 ) = ( 𝐺 ‘ 𝑆 ) ) )