ipolub

Description: The LUB of the inclusion poset. (hypotheses "ipolub.s" and "ipolub.t" could be eliminated with S e. dom U .) Could be significantly shortened if poslubdg is in quantified form. mrelatlub could potentially be shortened using this. See mrelatlubALT . (Contributed by Zhi Wang, 28-Sep-2024)

	Ref	Expression
Hypotheses	ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
	ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
	ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
	ipolub.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
	ipolubdm.t	⊢ ( 𝜑 → 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
	ipolub.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐹 )
Assertion	ipolub	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
4		ipolub.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
5		ipolubdm.t	⊢ ( 𝜑 → 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
6		ipolub.t	⊢ ( 𝜑 → 𝑇 ∈ 𝐹 )
7		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
8	1	ipobas	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 = ( Base ‘ 𝐼 ) )
9	2 8	syl	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐼 ) )
10	1	ipopos	⊢ 𝐼 ∈ Poset
11	10	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
12		breq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ( le ‘ 𝐼 ) 𝑇 ↔ 𝑦 ( le ‘ 𝐼 ) 𝑇 ) )
13		intubeu	⊢ ( 𝑇 ∈ 𝐹 → ( ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑣 → 𝑇 ⊆ 𝑣 ) ) ↔ 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } ) )
14	13	biimpar	⊢ ( ( 𝑇 ∈ 𝐹 ∧ 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } ) → ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑣 → 𝑇 ⊆ 𝑣 ) ) )
15	6 5 14	syl2anc	⊢ ( 𝜑 → ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑣 → 𝑇 ⊆ 𝑣 ) ) )
16	1 2 3 7	ipolublem	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → ( ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑣 → 𝑇 ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) ) ) )
17	6 16	mpdan	⊢ ( 𝜑 → ( ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑣 → 𝑇 ⊆ 𝑣 ) ) ↔ ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) ) ) )
18	15 17	mpbid	⊢ ( 𝜑 → ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑇 ∧ ∀ 𝑣 ∈ 𝐹 ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) ) )
19	18	simpld	⊢ ( 𝜑 → ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑇 )
20	19	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑇 )
21		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ∈ 𝑆 )
22	12 20 21	rspcdva	⊢ ( ( 𝜑 ∧ 𝑦 ∈ 𝑆 ) → 𝑦 ( le ‘ 𝐼 ) 𝑇 )
23		breq2	⊢ ( 𝑣 = 𝑧 → ( 𝑤 ( le ‘ 𝐼 ) 𝑣 ↔ 𝑤 ( le ‘ 𝐼 ) 𝑧 ) )
24	23	ralbidv	⊢ ( 𝑣 = 𝑧 → ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 ↔ ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑧 ) )
25		breq1	⊢ ( 𝑤 = 𝑦 → ( 𝑤 ( le ‘ 𝐼 ) 𝑧 ↔ 𝑦 ( le ‘ 𝐼 ) 𝑧 ) )
26	25	cbvralvw	⊢ ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 )
27	24 26	bitrdi	⊢ ( 𝑣 = 𝑧 → ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 ) )
28		breq2	⊢ ( 𝑣 = 𝑧 → ( 𝑇 ( le ‘ 𝐼 ) 𝑣 ↔ 𝑇 ( le ‘ 𝐼 ) 𝑧 ) )
29	27 28	imbi12d	⊢ ( 𝑣 = 𝑧 → ( ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 → 𝑇 ( le ‘ 𝐼 ) 𝑧 ) ) )
30	18	simprd	⊢ ( 𝜑 → ∀ 𝑣 ∈ 𝐹 ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) )
31	30	adantr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐹 ) → ∀ 𝑣 ∈ 𝐹 ( ∀ 𝑤 ∈ 𝑆 𝑤 ( le ‘ 𝐼 ) 𝑣 → 𝑇 ( le ‘ 𝐼 ) 𝑣 ) )
32		simpr	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐹 ) → 𝑧 ∈ 𝐹 )
33	29 31 32	rspcdva	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐹 ) → ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 → 𝑇 ( le ‘ 𝐼 ) 𝑧 ) )
34	33	3impia	⊢ ( ( 𝜑 ∧ 𝑧 ∈ 𝐹 ∧ ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 ) → 𝑇 ( le ‘ 𝐼 ) 𝑧 )
35	7 9 4 11 3 6 22 34	poslubdg	⊢ ( 𝜑 → ( 𝑈 ‘ 𝑆 ) = 𝑇 )

Metamath Proof Explorer

Theorem ipolub

Proof