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

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 𝑈 } )