Metamath Proof Explorer

Theorem intubeu

Description: Existential uniqueness of the least upper bound. (Contributed by Zhi Wang, 28-Sep-2024)

Ref Expression
Assertion intubeu ⊢ C ∈ B → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y ↔ C = ⋂ x ∈ B | A ⊆ x

Proof

Step Hyp Ref Expression
1 ssint ⊢ C ⊆ ⋂ x ∈ B | A ⊆ x ↔ ∀ y ∈ x ∈ B | A ⊆ x C ⊆ y
2 sseq2 ⊢ x = y → A ⊆ x ↔ A ⊆ y
3 2 ralrab ⊢ ∀ y ∈ x ∈ B | A ⊆ x C ⊆ y ↔ ∀ y ∈ B A ⊆ y → C ⊆ y
4 1 3 bitri ⊢ C ⊆ ⋂ x ∈ B | A ⊆ x ↔ ∀ y ∈ B A ⊆ y → C ⊆ y
5 4 bilanri ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ⊆ ⋂ x ∈ B | A ⊆ x
6 sseq2 ⊢ z = C → A ⊆ z ↔ A ⊆ C
7 simpll ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ B
8 simplr ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → A ⊆ C
9 6 7 8 elrabd ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ z ∈ B | A ⊆ z
10 sseq2 ⊢ z = x → A ⊆ z ↔ A ⊆ x
11 10 cbvrabv ⊢ z ∈ B | A ⊆ z = x ∈ B | A ⊆ x
12 9 11 eleqtrdi ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ x ∈ B | A ⊆ x
13 intss1 ⊢ C ∈ x ∈ B | A ⊆ x → ⋂ x ∈ B | A ⊆ x ⊆ C
14 12 13 syl ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → ⋂ x ∈ B | A ⊆ x ⊆ C
15 5 14 eqssd ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C = ⋂ x ∈ B | A ⊆ x
16 15 expl ⊢ C ∈ B → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C = ⋂ x ∈ B | A ⊆ x
17 ssintub ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x
18 sseq2 ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C ↔ A ⊆ ⋂ x ∈ B | A ⊆ x
19 17 18 mpbiri ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C
20 eqimss ⊢ C = ⋂ x ∈ B | A ⊆ x → C ⊆ ⋂ x ∈ B | A ⊆ x
21 20 4 sylib ⊢ C = ⋂ x ∈ B | A ⊆ x → ∀ y ∈ B A ⊆ y → C ⊆ y
22 19 21 jca ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y
23 16 22 impbid1 ⊢ C ∈ B → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y ↔ C = ⋂ x ∈ B | A ⊆ x