lejoin1

Description: A join's first argument is less than or equal to the join. (Contributed by NM, 16-Sep-2011)

	Ref	Expression
Hypotheses	joinval2.b	$⊢ B = {Base}_{K}$
	joinval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	joinval2.j	$⊢ \underset{˙}{\lor} = join (K)$
	joinval2.k	$⊢ φ \to K \in V$
	joinval2.x	$⊢ φ \to X \in B$
	joinval2.y	$⊢ φ \to Y \in B$
	joinlem.e	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
Assertion	lejoin1	$⊢ φ \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$

Step	Hyp	Ref	Expression
1		joinval2.b	$⊢ B = {Base}_{K}$
2		joinval2.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		joinval2.j	$⊢ \underset{˙}{\lor} = join (K)$
4		joinval2.k	$⊢ φ \to K \in V$
5		joinval2.x	$⊢ φ \to X \in B$
6		joinval2.y	$⊢ φ \to Y \in B$
7		joinlem.e	$⊢ φ \to ⟨X, Y⟩ \in dom \underset{˙}{\lor}$
8	1 2 3 4 5 6 7	joinlem	$⊢ φ \to ((X \underset{˙}{\leq} (X \underset{˙}{\lor} Y) \land Y \underset{˙}{\leq} (X \underset{˙}{\lor} Y)) \land \forall z \in B ((X \underset{˙}{\leq} z \land Y \underset{˙}{\leq} z) \to (X \underset{˙}{\lor} Y) \underset{˙}{\leq} z))$
9	8	simplld	$⊢ φ \to X \underset{˙}{\leq} (X \underset{˙}{\lor} Y)$

Metamath Proof Explorer