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

Metamath Proof Explorer

Theorem lubsscl

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

Ref Expression
Hypotheses lubsscl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
lubsscl.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
lubsscl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubsscl.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
lubsscl.x ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝑇 )
Assertion lubsscl ( 𝜑 → ( 𝑇 ∈ dom 𝑈 ∧ ( 𝑈 ‘ 𝑇 ) = ( 𝑈 ‘ 𝑆 ) ) )

Proof

Step Hyp Ref Expression
1 lubsscl.k ⊢ ( 𝜑 → 𝐾 ∈ Poset )
2 lubsscl.t ⊢ ( 𝜑 → 𝑇 ⊆ 𝑆 )
3 lubsscl.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubsscl.s ⊢ ( 𝜑 → 𝑆 ∈ dom 𝑈 )
5 lubsscl.x ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) ∈ 𝑇 )
6 eqid ⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
7 eqid ⊢ ( le ‘ 𝐾 ) = ( le ‘ 𝐾 )
8 6 7 3 1 4 lubelss ⊢ ( 𝜑 → 𝑆 ⊆ ( 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 luble ⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑇 ) → 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) )
15 14 ralrimiva ⊢ ( 𝜑 → ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) )
16 breq1 ⊢ ( 𝑦 = ( 𝑈 ‘ 𝑆 ) → ( 𝑦 ( 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 breq2 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) ) )
23 22 ralbidv ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 ↔ ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) ( 𝑈 ‘ 𝑆 ) ) )
24 breq1 ⊢ ( 𝑥 = ( 𝑈 ‘ 𝑆 ) → ( 𝑥 ( 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 lubeldm2 ⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝑈 ↔ ( 𝑇 ⊆ ( Base ‘ 𝐾 ) ∧ ∃ 𝑥 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑥 ∧ ∀ 𝑧 ∈ ( Base ‘ 𝐾 ) ( ∀ 𝑦 ∈ 𝑇 𝑦 ( le ‘ 𝐾 ) 𝑧 → 𝑥 ( le ‘ 𝐾 ) 𝑧 ) ) ) ) )
32 9 29 31 mpbir2and ⊢ ( 𝜑 → 𝑇 ∈ dom 𝑈 )
33 7 6 3 1 9 10 14 19 poslubd ⊢ ( 𝜑 → ( 𝑈 ‘ 𝑇 ) = ( 𝑈 ‘ 𝑆 ) )
34 32 33 jca ⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝑈 ∧ ( 𝑈 ‘ 𝑇 ) = ( 𝑈 ‘ 𝑆 ) ) )