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 biimpri ⊢ ∀ y ∈ B y ⊆ A → y ⊆ C → ⋃ x ∈ B | x ⊆ A ⊆ C
15 14 adantl ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → ⋃ x ∈ B | x ⊆ A ⊆ C
16 9 15 eqssd ⊢ C ∈ B ∧ C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C → C = ⋃ x ∈ B | x ⊆ A
17 16 expl ⊢ C ∈ B → C ⊆ A ∧ ∀ y ∈ B y ⊆ 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 ∈ B y ⊆ A → y ⊆ C
23 20 22 jca ⊢ C = ⋃ x ∈ B | x ⊆ A → C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C
24 17 23 impbid1 ⊢ C ∈ B → C ⊆ A ∧ ∀ y ∈ B y ⊆ A → y ⊆ C ↔ C = ⋃ x ∈ B | x ⊆ A