joindef

Description: Two ways to say that a join is defined. (Contributed by NM, 9-Sep-2018)

	Ref	Expression
Hypotheses	joindef.u	$⊢ U = lub (K)$
	joindef.j	$⊢ \underset{˙}{\lor} = join (K)$
	joindef.k	$⊢ φ \to K \in V$
	joindef.x	$⊢ φ \to X \in W$
	joindef.y	$⊢ φ \to Y \in Z$
Assertion	joindef	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow \{X, Y\} \in dom U)$

Step	Hyp	Ref	Expression
1		joindef.u	$⊢ U = lub (K)$
2		joindef.j	$⊢ \underset{˙}{\lor} = join (K)$
3		joindef.k	$⊢ φ \to K \in V$
4		joindef.x	$⊢ φ \to X \in W$
5		joindef.y	$⊢ φ \to Y \in Z$
6	1 2	joindm	$⊢ K \in V \to dom \underset{˙}{\lor} = \{⟨x, y⟩ \| \{x, y\} \in dom U\}$
7	6	eleq2d	$⊢ K \in V \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom U\})$
8	3 7	syl	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom U\})$
9		preq1	$⊢ x = X \to \{x, y\} = \{X, y\}$
10	9	eleq1d	$⊢ x = X \to (\{x, y\} \in dom U \leftrightarrow \{X, y\} \in dom U)$
11		preq2	$⊢ y = Y \to \{X, y\} = \{X, Y\}$
12	11	eleq1d	$⊢ y = Y \to (\{X, y\} \in dom U \leftrightarrow \{X, Y\} \in dom U)$
13	10 12	opelopabg	$⊢ (X \in W \land Y \in Z) \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom U\} \leftrightarrow \{X, Y\} \in dom U)$
14	4 5 13	syl2anc	$⊢ φ \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| \{x, y\} \in dom U\} \leftrightarrow \{X, Y\} \in dom U)$
15	8 14	bitrd	$⊢ φ \to (⟨X, Y⟩ \in dom \underset{˙}{\lor} \leftrightarrow \{X, Y\} \in dom U)$

Metamath Proof Explorer