Metamath Proof Explorer

Theorem lubeldm

Description: Member of the domain of the least upper bound function of a poset. (Contributed by NM, 7-Sep-2018)

Ref Expression
Hypotheses lubeldm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubeldm.l ⊢ ≤ = ( le ‘ 𝐾 )
lubeldm.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubeldm.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
lubeldm.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion lubeldm ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )

Proof

Step Hyp Ref Expression
1 lubeldm.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubeldm.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubeldm.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubeldm.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
5 lubeldm.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6 biid ⊢ ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
7 1 2 3 6 5 lubdm ⊢ ( 𝜑 → dom 𝑈 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } )
8 7 eleq2d ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ) )
9 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ) )
10 raleq ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 ↔ ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 ) )
11 10 imbi1d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
12 11 ralbidv ⊢ ( 𝑠 = 𝑆 → ( ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ↔ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
13 9 12 anbi12d ⊢ ( 𝑠 = 𝑆 → ( ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
14 13 reubidv ⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ) )
15 4 reubii ⊢ ( ∃! 𝑥 ∈ 𝐵 𝜓 ↔ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑆 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
16 14 15 bitr4di ⊢ ( 𝑠 = 𝑆 → ( ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) ↔ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
17 16 elrab ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ↔ ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
18 1 fvexi ⊢ 𝐵 ∈ V
19 18 elpw2 ⊢ ( 𝑆 ∈ 𝒫 𝐵 ↔ 𝑆 ⊆ 𝐵 )
20 19 anbi1i ⊢ ( ( 𝑆 ∈ 𝒫 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
21 17 20 bitri ⊢ ( 𝑆 ∈ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) } ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) )
22 8 21 bitrdi ⊢ ( 𝜑 → ( 𝑆 ∈ dom 𝑈 ↔ ( 𝑆 ⊆ 𝐵 ∧ ∃! 𝑥 ∈ 𝐵 𝜓 ) ) )