This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem intubeu

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

Ref Expression
Assertion intubeu ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) ↔ 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )

Proof

Step Hyp Ref Expression
1 ssint ⊢ ( 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } 𝐶 ⊆ 𝑦 )
2 sseq2 ⊢ ( 𝑥 = 𝑦 → ( 𝐴 ⊆ 𝑥 ↔ 𝐴 ⊆ 𝑦 ) )
3 2 ralrab ⊢ ( ∀ 𝑦 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } 𝐶 ⊆ 𝑦 ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
4 1 3 bitri ⊢ ( 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ↔ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
5 4 biimpri ⊢ ( ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
6 5 adantl ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
7 sseq2 ⊢ ( 𝑧 = 𝐶 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝐶 ) )
8 simpll ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ 𝐵 )
9 simplr ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐴 ⊆ 𝐶 )
10 7 8 9 elrabd ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } )
11 sseq2 ⊢ ( 𝑧 = 𝑥 → ( 𝐴 ⊆ 𝑧 ↔ 𝐴 ⊆ 𝑥 ) )
12 11 cbvrabv ⊢ { 𝑧 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑧 } = { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
13 10 12 eleqtrdi ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
14 intss1 ⊢ ( 𝐶 ∈ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
15 13 14 syl ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ⊆ 𝐶 )
16 6 15 eqssd ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐴 ⊆ 𝐶 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
17 16 expl ⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) → 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
18 ssintub ⊢ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 }
19 sseq2 ⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ↔ 𝐴 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )
20 18 19 mpbiri ⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐴 ⊆ 𝐶 )
21 eqimss ⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → 𝐶 ⊆ ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } )
22 21 4 sylib ⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) )
23 20 22 jca ⊢ ( 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } → ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) )
24 17 23 impbid1 ⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐴 ⊆ 𝐶 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝐴 ⊆ 𝑦 → 𝐶 ⊆ 𝑦 ) ) ↔ 𝐶 = ∩ { 𝑥 ∈ 𝐵 ∣ 𝐴 ⊆ 𝑥 } ) )