Metamath Proof Explorer

Theorem unilbeu

Description: Existential uniqueness of the greatest lower bound. (Contributed by Zhi Wang, 29-Sep-2024)

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

Proof

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