1cvratlt

Description: An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012)

	Ref	Expression
Hypotheses	1cvratlt.b	$⊢ B = {Base}_{K}$
	1cvratlt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	1cvratlt.s	$⊢ \underset{˙}{<} = <_{K}$
	1cvratlt.u	$⊢ \underset{˙}{1} = 1. (K)$
	1cvratlt.c	$⊢ C = ⋖_{K}$
	1cvratlt.a	$⊢ A = Atoms (K)$
Assertion	1cvratlt	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to P \underset{˙}{<} X$

Proof

Step	Hyp	Ref	Expression
1		1cvratlt.b	$⊢ B = {Base}_{K}$
2		1cvratlt.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		1cvratlt.s	$⊢ \underset{˙}{<} = <_{K}$
4		1cvratlt.u	$⊢ \underset{˙}{1} = 1. (K)$
5		1cvratlt.c	$⊢ C = ⋖_{K}$
6		1cvratlt.a	$⊢ A = Atoms (K)$
7		simpl1	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to K \in HL$
8		simpl3	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to X \in B$
9		simprl	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to X C \underset{˙}{1}$
10	1 3 4 5 6	1cvratex	$⊢ (K \in HL \land X \in B \land X C \underset{˙}{1}) \to \exists q \in A q \underset{˙}{<} X$
11	7 8 9 10	syl3anc	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to \exists q \in A q \underset{˙}{<} X$
12		simp1l1	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to K \in HL$
13		simp1l2	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to P \in A$
14		simp2	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to q \in A$
15		simp1l3	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to X \in B$
16		simp1rr	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to P \underset{˙}{\leq} X$
17		simp3	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to q \underset{˙}{<} X$
18	1 2 3 6	atlelt	$⊢ (K \in HL \land (P \in A \land q \in A \land X \in B) \land (P \underset{˙}{\leq} X \land q \underset{˙}{<} X)) \to P \underset{˙}{<} X$
19	12 13 14 15 16 17 18	syl132anc	$⊢ (((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \land q \in A \land q \underset{˙}{<} X) \to P \underset{˙}{<} X$
20	19	rexlimdv3a	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to (\exists q \in A q \underset{˙}{<} X \to P \underset{˙}{<} X)$
21	11 20	mpd	$⊢ ((K \in HL \land P \in A \land X \in B) \land (X C \underset{˙}{1} \land P \underset{˙}{\leq} X)) \to P \underset{˙}{<} X$

Metamath Proof Explorer

Theorem 1cvratlt

Proof