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∈BA⊆y→C⊆y↔C=⋂x∈B|A⊆x

Proof

Step Hyp Ref Expression
1 ssint ⊢C⊆⋂x∈B|A⊆x↔∀y∈x∈B|A⊆xC⊆y
2 sseq2 ⊢x=y→A⊆x↔A⊆y
3 2 ralrab ⊢∀y∈x∈B|A⊆xC⊆y↔∀y∈BA⊆y→C⊆y
4 1 3 bitri ⊢C⊆⋂x∈B|A⊆x↔∀y∈BA⊆y→C⊆y
5 4 biimpri ⊢∀y∈BA⊆y→C⊆y→C⊆⋂x∈B|A⊆x
6 5 adantl ⊢C∈B∧A⊆C∧∀y∈BA⊆y→C⊆y→C⊆⋂x∈B|A⊆x
7 sseq2 ⊢z=C→A⊆z↔A⊆C
8 simpll ⊢C∈B∧A⊆C∧∀y∈BA⊆y→C⊆y→C∈B
9 simplr ⊢C∈B∧A⊆C∧∀y∈BA⊆y→C⊆y→A⊆C
10 7 8 9 elrabd ⊢C∈B∧A⊆C∧∀y∈BA⊆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∈BA⊆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∈BA⊆y→C⊆y→⋂x∈B|A⊆x⊆C
16 6 15 eqssd ⊢C∈B∧A⊆C∧∀y∈BA⊆y→C⊆y→C=⋂x∈B|A⊆x
17 16 expl ⊢C∈B→A⊆C∧∀y∈BA⊆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∈BA⊆y→C⊆y
23 20 22 jca ⊢C=⋂x∈B|A⊆x→A⊆C∧∀y∈BA⊆y→C⊆y
24 17 23 impbid1 ⊢C∈B→A⊆C∧∀y∈BA⊆y→C⊆y↔C=⋂x∈B|A⊆x