ipolubdm

Description: The domain of the LUB of the inclusion poset. (Contributed by Zhi Wang, 28-Sep-2024)

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

Proof

Step	Hyp	Ref	Expression
1		ipolub.i	⊢ 𝐼 = ( toInc ‘ 𝐹 )
2		ipolub.f	⊢ ( 𝜑 → 𝐹 ∈ 𝑉 )
3		ipolub.s	⊢ ( 𝜑 → 𝑆 ⊆ 𝐹 )
4		ipolub.u	⊢ ( 𝜑 → 𝑈 = ( lub ‘ 𝐼 ) )
5		ipolubdm.t	⊢ ( 𝜑 → 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
6	1	ipobas	⊢ ( 𝐹 ∈ 𝑉 → 𝐹 = ( Base ‘ 𝐼 ) )
7	2 6	syl	⊢ ( 𝜑 → 𝐹 = ( Base ‘ 𝐼 ) )
8		eqidd	⊢ ( 𝜑 → ( le ‘ 𝐼 ) = ( le ‘ 𝐼 ) )
9		eqid	⊢ ( le ‘ 𝐼 ) = ( le ‘ 𝐼 )
10	1 2 3 9	ipolublem	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) → ( ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∀ 𝑦 ∈ 𝑆 𝑦 ( le ‘ 𝐼 ) 𝑧 → 𝑡 ( le ‘ 𝐼 ) 𝑧 ) ) ) )
11	1	ipopos	⊢ 𝐼 ∈ Poset
12	11	a1i	⊢ ( 𝜑 → 𝐼 ∈ Poset )
13	7 8 4 10 12	lubeldm2d	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐹 ∧ ∃ 𝑡 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) ) )
14	3 13	mpbirand	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ∃ 𝑡 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) )
15	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
16		intubeu	⊢ ( 𝑡 ∈ 𝐹 → ( ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ↔ 𝑡 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } ) )
17	16	biimpa	⊢ ( ( 𝑡 ∈ 𝐹 ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑡 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
18	17	adantll	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑡 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } )
19	15 18	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑇 = 𝑡 )
20		simplr	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑡 ∈ 𝐹 )
21	19 20	eqeltrd	⊢ ( ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) ∧ ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ) → 𝑇 ∈ 𝐹 )
22	21	ex	⊢ ( ( 𝜑 ∧ 𝑡 ∈ 𝐹 ) → ( ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) → 𝑇 ∈ 𝐹 ) )
23		simpr	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → 𝑇 ∈ 𝐹 )
24		intubeu	⊢ ( 𝑇 ∈ 𝐹 → ( ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) ↔ 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } ) )
25	24	biimparc	⊢ ( ( 𝑇 = ∩ { 𝑥 ∈ 𝐹 ∣ ∪ 𝑆 ⊆ 𝑥 } ∧ 𝑇 ∈ 𝐹 ) → ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) )
26	5 25	sylan	⊢ ( ( 𝜑 ∧ 𝑇 ∈ 𝐹 ) → ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) )
27		sseq2	⊢ ( 𝑡 = 𝑇 → ( ∪ 𝑆 ⊆ 𝑡 ↔ ∪ 𝑆 ⊆ 𝑇 ) )
28		sseq1	⊢ ( 𝑡 = 𝑇 → ( 𝑡 ⊆ 𝑧 ↔ 𝑇 ⊆ 𝑧 ) )
29	28	imbi2d	⊢ ( 𝑡 = 𝑇 → ( ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ↔ ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) )
30	29	ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) )
31	27 30	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ↔ ( ∪ 𝑆 ⊆ 𝑇 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑇 ⊆ 𝑧 ) ) ) )
32	22 23 26 31	rspceb2dv	⊢ ( 𝜑 → ( ∃ 𝑡 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑡 ∧ ∀ 𝑧 ∈ 𝐹 ( ∪ 𝑆 ⊆ 𝑧 → 𝑡 ⊆ 𝑧 ) ) ↔ 𝑇 ∈ 𝐹 ) )
33	14 32	bitrd	⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ 𝑇 ∈ 𝐹 ) )

Metamath Proof Explorer

Theorem ipolubdm

Proof