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

Metamath Proof Explorer

Theorem lubdm

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

Ref Expression
Hypotheses lubfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
lubfval.l ⊢ ≤ = ( le ‘ 𝐾 )
lubfval.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
lubfval.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
lubfval.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
Assertion lubdm ( 𝜑 → dom 𝑈 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } )

Proof

Step Hyp Ref Expression
1 lubfval.b ⊢ 𝐵 = ( Base ‘ 𝐾 )
2 lubfval.l ⊢ ≤ = ( le ‘ 𝐾 )
3 lubfval.u ⊢ 𝑈 = ( lub ‘ 𝐾 )
4 lubfval.p ⊢ ( 𝜓 ↔ ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑥 ∧ ∀ 𝑧 ∈ 𝐵 ( ∀ 𝑦 ∈ 𝑠 𝑦 ≤ 𝑧 → 𝑥 ≤ 𝑧 ) ) )
5 lubfval.k ⊢ ( 𝜑 → 𝐾 ∈ 𝑉 )
6 1 2 3 4 5 lubfval ⊢ ( 𝜑 → 𝑈 = ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )
7 6 dmeqd ⊢ ( 𝜑 → dom 𝑈 = dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) )
8 riotaex ⊢ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ∈ V
9 eqid ⊢ ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) )
10 8 9 dmmpti ⊢ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) = 𝒫 𝐵
11 10 ineq2i ⊢ ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ) = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ 𝒫 𝐵 )
12 dmres ⊢ dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ dom ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) )
13 dfrab2 ⊢ { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } = ( { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ∩ 𝒫 𝐵 )
14 11 12 13 3eqtr4i ⊢ dom ( ( 𝑠 ∈ 𝒫 𝐵 ↦ ( ℩ 𝑥 ∈ 𝐵 𝜓 ) ) ↾ { 𝑠 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } ) = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 }
15 7 14 eqtrdi ⊢ ( 𝜑 → dom 𝑈 = { 𝑠 ∈ 𝒫 𝐵 ∣ ∃! 𝑥 ∈ 𝐵 𝜓 } )