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 ∈ B y ⊆ 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 ∈ B y ⊆ A → y ⊆ C → C ∈ B
3 simplr ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → C ⊆ A
4 1 2 3 elrabd ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ 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 ∈ B y ⊆ 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 ∈ B y ⊆ A → y ⊆ C → C ⊆ ⋃ x ∈ B | x ⊆ A
10 unissb ⊢ ⋃ x ∈ B | x ⊆ A ⊆ C ↔ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ C
11 sseq1 ⊢ x = y → x ⊆ A ↔ y ⊆ A
12 11 ralrab ⊢ ∀ y ∈ x ∈ B | x ⊆ A y ⊆ C ↔ ∀ y ∈ B y ⊆ A → y ⊆ C
13 10 12 bitri ⊢ ⋃ x ∈ B | x ⊆ A ⊆ C ↔ ∀ y ∈ B y ⊆ A → y ⊆ C
14 13 bilanri ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → ⋃ x ∈ B | x ⊆ A ⊆ C
15 9 14 eqssd ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → C = ⋃ x ∈ B | x ⊆ A
16 15 expl ⊢ C ∈ B → C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → C = ⋃ x ∈ B | x ⊆ A
17 unilbss ⊢ ⋃ x ∈ B | x ⊆ A ⊆ A
18 sseq1 ⊢ C = ⋃ x ∈ B | x ⊆ A → C ⊆ A ↔ ⋃ x ∈ B | x ⊆ A ⊆ A
19 17 18 mpbiri ⊢ C = ⋃ x ∈ B | x ⊆ A → C ⊆ A
20 eqimss2 ⊢ C = ⋃ x ∈ B | x ⊆ A → ⋃ x ∈ B | x ⊆ A ⊆ C
21 20 13 sylib ⊢ C = ⋃ x ∈ B | x ⊆ A → ∀ y ∈ B y ⊆ A → y ⊆ C
22 19 21 jca ⊢ C = ⋃ x ∈ B | x ⊆ A → C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C
23 16 22 impbid1 ⊢ C ∈ B → C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C ↔ C = ⋃ x ∈ B | x ⊆ A