paddasslem3

Description: Lemma for paddass . Restate projective space axiom ps-2 . (Contributed by NM, 8-Jan-2012)

	Ref	Expression
Hypotheses	paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
	paddasslem.a	$⊢ A = Atoms (K)$
Assertion	paddasslem3	$⊢ (K \in HL \land (x \in A \land r \in A \land y \in A) \land (p \in A \land z \in A)) \to (((\neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y) \land p \neq z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))$

Step	Hyp	Ref	Expression
1		paddasslem.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
2		paddasslem.j	$⊢ \underset{˙}{\lor} = join (K)$
3		paddasslem.a	$⊢ A = Atoms (K)$
4	1 2 3	ps-2	$⊢ ((K \in HL \land (x \in A \land r \in A \land y \in A) \land (p \in A \land z \in A)) \land ((\neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y) \land p \neq z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y)))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z))$
5	4	ex	$⊢ (K \in HL \land (x \in A \land r \in A \land y \in A) \land (p \in A \land z \in A)) \to (((\neg x \underset{˙}{\leq} (r \underset{˙}{\lor} y) \land p \neq z) \land (p \underset{˙}{\leq} (x \underset{˙}{\lor} r) \land z \underset{˙}{\leq} (r \underset{˙}{\lor} y))) \to \exists s \in A (s \underset{˙}{\leq} (x \underset{˙}{\lor} y) \land s \underset{˙}{\leq} (p \underset{˙}{\lor} z)))$

Metamath Proof Explorer