Metamath Proof Explorer

Theorem unilbeu

Description: Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024)

Ref Expression
Assertion unilbeu ⊢C∈B→C⊆A∧∀y∈By⊆A→y⊆C↔C=⋃x∈B|x⊆A

Proof

Step Hyp Ref Expression
1 sseq1 ⊢z=C→z⊆A↔C⊆A
2 simpll ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C∈B
3 simplr ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C⊆A
4 1 2 3 elrabd ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C∈z∈B|z⊆A
5 sseq1 ⊢z=x→z⊆A↔x⊆A
6 5 cbvrabv ⊢z∈B|z⊆A=x∈B|x⊆A
7 4 6 eleqtrdi ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C∈x∈B|x⊆A
8 elssuni ⊢C∈x∈B|x⊆A→C⊆⋃x∈B|x⊆A
9 7 8 syl ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C⊆⋃x∈B|x⊆A
10 unissb ⊢⋃x∈B|x⊆A⊆C↔∀y∈x∈B|x⊆Ay⊆C
11 sseq1 ⊢x=y→x⊆A↔y⊆A
12 11 ralrab ⊢∀y∈x∈B|x⊆Ay⊆C↔∀y∈By⊆A→y⊆C
13 10 12 bitri ⊢⋃x∈B|x⊆A⊆C↔∀y∈By⊆A→y⊆C
14 13 biimpri ⊢∀y∈By⊆A→y⊆C→⋃x∈B|x⊆A⊆C
15 14 adantl ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→⋃x∈B|x⊆A⊆C
16 9 15 eqssd ⊢C∈B∧C⊆A∧∀y∈By⊆A→y⊆C→C=⋃x∈B|x⊆A
17 16 expl ⊢C∈B→C⊆A∧∀y∈By⊆A→y⊆C→C=⋃x∈B|x⊆A
18 unilbss ⊢⋃x∈B|x⊆A⊆A
19 sseq1 ⊢C=⋃x∈B|x⊆A→C⊆A↔⋃x∈B|x⊆A⊆A
20 18 19 mpbiri ⊢C=⋃x∈B|x⊆A→C⊆A
21 eqimss2 ⊢C=⋃x∈B|x⊆A→⋃x∈B|x⊆A⊆C
22 21 13 sylib ⊢C=⋃x∈B|x⊆A→∀y∈By⊆A→y⊆C
23 20 22 jca ⊢C=⋃x∈B|x⊆A→C⊆A∧∀y∈By⊆A→y⊆C
24 17 23 impbid1 ⊢C∈B→C⊆A∧∀y∈By⊆A→y⊆C↔C=⋃x∈B|x⊆A