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 bilanri ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) ) → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐶 )
15 9 14 eqssd ⊢ ( ( ( 𝐶 ∈ 𝐵 ∧ 𝐶 ⊆ 𝐴 ) ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) ) → 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } )
16 15 expl ⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐶 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) ) → 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ) )
17 unilbss ⊢ ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐴
18 sseq1 ⊢ ( 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → ( 𝐶 ⊆ 𝐴 ↔ ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐴 ) )
19 17 18 mpbiri ⊢ ( 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → 𝐶 ⊆ 𝐴 )
20 eqimss2 ⊢ ( 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ⊆ 𝐶 )
21 20 13 sylib ⊢ ( 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) )
22 19 21 jca ⊢ ( 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } → ( 𝐶 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) ) )
23 16 22 impbid1 ⊢ ( 𝐶 ∈ 𝐵 → ( ( 𝐶 ⊆ 𝐴 ∧ ∀ 𝑦 ∈ 𝐵 ( 𝑦 ⊆ 𝐴 → 𝑦 ⊆ 𝐶 ) ) ↔ 𝐶 = ∪ { 𝑥 ∈ 𝐵 ∣ 𝑥 ⊆ 𝐴 } ) )