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	posglbd	⊢ ( 𝜑 → ( 𝐺 ‘ 𝑇 ) = ( 𝐺 ‘ 𝑆 ) )
36	32 35	jca	⊢ ( 𝜑 → ( 𝑇 ∈ dom 𝐺 ∧ ( 𝐺 ‘ 𝑇 ) = ( 𝐺 ‘ 𝑆 ) ) )

Metamath Proof Explorer

Theorem glbsscl

Proof