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 biimpri ⊢ ∀ y ∈ B A ⊆ y → C ⊆ y → C ⊆ ⋂ x ∈ B | A ⊆ x
6 5 adantl ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ⊆ ⋂ x ∈ B | A ⊆ x
7 sseq2 ⊢ z = C → A ⊆ z ↔ A ⊆ C
8 simpll ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ B
9 simplr ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → A ⊆ C
10 7 8 9 elrabd ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ z ∈ B | A ⊆ z
11 sseq2 ⊢ z = x → A ⊆ z ↔ A ⊆ x
12 11 cbvrabv ⊢ z ∈ B | A ⊆ z = x ∈ B | A ⊆ x
13 10 12 eleqtrdi ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C ∈ x ∈ B | A ⊆ x
14 intss1 ⊢ C ∈ x ∈ B | A ⊆ x → ⋂ x ∈ B | A ⊆ x ⊆ C
15 13 14 syl ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → ⋂ x ∈ B | A ⊆ x ⊆ C
16 6 15 eqssd ⊢ C ∈ B ∧ A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C = ⋂ x ∈ B | A ⊆ x
17 16 expl ⊢ C ∈ B → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y → C = ⋂ x ∈ B | A ⊆ x
18 ssintub ⊢ A ⊆ ⋂ x ∈ B | A ⊆ x
19 sseq2 ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C ↔ A ⊆ ⋂ x ∈ B | A ⊆ x
20 18 19 mpbiri ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C
21 eqimss ⊢ C = ⋂ x ∈ B | A ⊆ x → C ⊆ ⋂ x ∈ B | A ⊆ x
22 21 4 sylib ⊢ C = ⋂ x ∈ B | A ⊆ x → ∀ y ∈ B A ⊆ y → C ⊆ y
23 20 22 jca ⊢ C = ⋂ x ∈ B | A ⊆ x → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y
24 17 23 impbid1 ⊢ C ∈ B → A ⊆ C ∧ ∀ y ∈ B A ⊆ y → C ⊆ y ↔ C = ⋂ x ∈ B | A ⊆ x