0ltat

	Ref	Expression
Hypotheses	0ltat.z	$⊢ \underset{˙}{0} = 0. (K)$
	0ltat.s	$⊢ \underset{˙}{<} = <_{K}$
	0ltat.a	$⊢ A = Atoms (K)$
Assertion	0ltat	$⊢ (K \in OP \land P \in A) \to \underset{˙}{0} \underset{˙}{<} P$

Step	Hyp	Ref	Expression
1		0ltat.z	$⊢ \underset{˙}{0} = 0. (K)$
2		0ltat.s	$⊢ \underset{˙}{<} = <_{K}$
3		0ltat.a	$⊢ A = Atoms (K)$
4		simpl	$⊢ (K \in OP \land P \in A) \to K \in OP$
5		eqid	$⊢ {Base}_{K} = {Base}_{K}$
6	5 1	op0cl	$⊢ K \in OP \to \underset{˙}{0} \in {Base}_{K}$
7	6	adantr	$⊢ (K \in OP \land P \in A) \to \underset{˙}{0} \in {Base}_{K}$
8	5 3	atbase	$⊢ P \in A \to P \in {Base}_{K}$
9	8	adantl	$⊢ (K \in OP \land P \in A) \to P \in {Base}_{K}$
10		eqid	$⊢ ⋖_{K} = ⋖_{K}$
11	1 10 3	atcvr0	$⊢ (K \in OP \land P \in A) \to \underset{˙}{0} ⋖_{K} P$
12	5 2 10	cvrlt	$⊢ ((K \in OP \land \underset{˙}{0} \in {Base}_{K} \land P \in {Base}_{K}) \land \underset{˙}{0} ⋖_{K} P) \to \underset{˙}{0} \underset{˙}{<} P$
13	4 7 9 11 12	syl31anc	$⊢ (K \in OP \land P \in A) \to \underset{˙}{0} \underset{˙}{<} P$

Metamath Proof Explorer