Theorem unilbss

Description: Superclass of the greatest lower bound. A dual statement of ssintub . (Contributed by Zhi Wang, 29-Sep-2024)

	Ref	Expression
Assertion	unilbss	⊢ ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐴

Proof

Step	Hyp	Ref	Expression
1		unissb	⊢ ( ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐴 ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } 𝑦 ⊆ 𝐴 )
2		sseq1	⊢ ( 𝑥 = 𝑦 → ( 𝑥 ⊆ 𝐴 ↔ 𝑦 ⊆ 𝐴 ) )
3	2	elrab	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ↔ ( 𝑦 ∈ 𝐵 ∧ 𝑦 ⊆ 𝐴 ) )
4	3	simprbi	⊢ ( 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → 𝑦 ⊆ 𝐴 )
5	1 4	mprgbir	⊢ ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐴