joindm

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

	Ref	Expression
Hypotheses	joinfval.u	$⊢ U = lub (K)$
	joinfval.j	$⊢ \underset{˙}{\lor} = join (K)$
Assertion	joindm	$⊢ K \in V \to dom \underset{˙}{\lor} = \{⟨x, y⟩ \| \{x, y\} \in dom U\}$

Step	Hyp	Ref	Expression
1		joinfval.u	$⊢ U = lub (K)$
2		joinfval.j	$⊢ \underset{˙}{\lor} = join (K)$
3	1 2	joinfval2	$⊢ K \in V \to \underset{˙}{\lor} = \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
4	3	dmeqd	$⊢ K \in V \to dom \underset{˙}{\lor} = dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
5		dmoprab	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} = \{⟨x, y⟩ \| \exists z (\{x, y\} \in dom U \land z = U (\{x, y\}))\}$
6		fvex	$⊢ U (\{x, y\}) \in V$
7	6	isseti	$⊢ \exists z z = U (\{x, y\})$
8		19.42v	$⊢ \exists z (\{x, y\} \in dom U \land z = U (\{x, y\})) \leftrightarrow (\{x, y\} \in dom U \land \exists z z = U (\{x, y\}))$
9	7 8	mpbiran2	$⊢ \exists z (\{x, y\} \in dom U \land z = U (\{x, y\})) \leftrightarrow \{x, y\} \in dom U$
10	9	opabbii	$⊢ \{⟨x, y⟩ \| \exists z (\{x, y\} \in dom U \land z = U (\{x, y\}))\} = \{⟨x, y⟩ \| \{x, y\} \in dom U\}$
11	5 10	eqtri	$⊢ dom \{⟨⟨x, y⟩, z⟩ \| (\{x, y\} \in dom U \land z = U (\{x, y\}))\} = \{⟨x, y⟩ \| \{x, y\} \in dom U\}$
12	4 11	eqtrdi	$⊢ K \in V \to dom \underset{˙}{\lor} = \{⟨x, y⟩ \| \{x, y\} \in dom U\}$

Metamath Proof Explorer