Metamath Proof Explorer


Theorem joindm

Description: Domain of join function for a poset-type structure. (Contributed by NM, 16-Sep-2018)

Ref Expression
Hypotheses joinfval.u 𝑈 = ( lub ‘ 𝐾 )
joinfval.j = ( join ‘ 𝐾 )
Assertion joindm ( 𝐾𝑉 → dom = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } )

Proof

Step Hyp Ref Expression
1 joinfval.u 𝑈 = ( lub ‘ 𝐾 )
2 joinfval.j = ( join ‘ 𝐾 )
3 1 2 joinfval2 ( 𝐾𝑉 = { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )
4 3 dmeqd ( 𝐾𝑉 → dom = dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } )
5 dmoprab dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) }
6 fvex ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ∈ V
7 6 isseti 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } )
8 19.42v ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ↔ ( { 𝑥 , 𝑦 } ∈ dom 𝑈 ∧ ∃ 𝑧 𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) )
9 7 8 mpbiran2 ( ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) ↔ { 𝑥 , 𝑦 } ∈ dom 𝑈 )
10 9 opabbii { ⟨ 𝑥 , 𝑦 ⟩ ∣ ∃ 𝑧 ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 }
11 5 10 eqtri dom { ⟨ ⟨ 𝑥 , 𝑦 ⟩ , 𝑧 ⟩ ∣ ( { 𝑥 , 𝑦 } ∈ dom 𝑈𝑧 = ( 𝑈 ‘ { 𝑥 , 𝑦 } ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 }
12 4 11 eqtrdi ( 𝐾𝑉 → dom = { ⟨ 𝑥 , 𝑦 ⟩ ∣ { 𝑥 , 𝑦 } ∈ dom 𝑈 } )