cvrval4N

Description: Binary relation expressing Y covers X . (Contributed by NM, 16-Jun-2012) (New usage is discouraged.)

	Ref	Expression
Hypotheses	cvrval4.b	$⊢ B = {Base}_{K}$
	cvrval4.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrval4.j	$⊢ \underset{˙}{\lor} = join (K)$
	cvrval4.c	$⊢ C = ⋖_{K}$
	cvrval4.a	$⊢ A = Atoms (K)$
Assertion	cvrval4N	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y))$

Proof

Step	Hyp	Ref	Expression
1		cvrval4.b	$⊢ B = {Base}_{K}$
2		cvrval4.s	$⊢ \underset{˙}{<} = <_{K}$
3		cvrval4.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrval4.c	$⊢ C = ⋖_{K}$
5		cvrval4.a	$⊢ A = Atoms (K)$
6	1 2 4	cvrlt	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to X \underset{˙}{<} Y$
7		eqid	$⊢ \leq_{K} = \leq_{K}$
8	1 7 3 4 5	cvrval3	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \exists p \in A (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y))$
9		simpr	$⊢ (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y) \to X \underset{˙}{\lor} p = Y$
10	9	reximi	$⊢ \exists p \in A (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y) \to \exists p \in A X \underset{˙}{\lor} p = Y$
11	8 10	syl6bi	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \to \exists p \in A X \underset{˙}{\lor} p = Y)$
12	11	imp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to \exists p \in A X \underset{˙}{\lor} p = Y$
13	6 12	jca	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y)$
14	13	ex	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \to (X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y))$
15		simp1r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to X \underset{˙}{<} Y$
16		simp3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to X \underset{˙}{\lor} p = Y$
17	15 16	breqtrrd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to X \underset{˙}{<} (X \underset{˙}{\lor} p)$
18		simp1l1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to K \in HL$
19		simp1l2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to X \in B$
20		simp2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to p \in A$
21	1 7 3 4 5	cvr1	$⊢ (K \in HL \land X \in B \land p \in A) \to (\neg p \leq_{K} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
22	18 19 20 21	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to (\neg p \leq_{K} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
23	1 2 3 4 5	cvr2N	$⊢ (K \in HL \land X \in B \land p \in A) \to (X \underset{˙}{<} (X \underset{˙}{\lor} p) \leftrightarrow X C (X \underset{˙}{\lor} p))$
24	18 19 20 23	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to (X \underset{˙}{<} (X \underset{˙}{\lor} p) \leftrightarrow X C (X \underset{˙}{\lor} p))$
25	22 24	bitr4d	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to (\neg p \leq_{K} X \leftrightarrow X \underset{˙}{<} (X \underset{˙}{\lor} p))$
26	17 25	mpbird	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to \neg p \leq_{K} X$
27	26 16	jca	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \land p \in A \land X \underset{˙}{\lor} p = Y) \to (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y)$
28	27	3exp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (p \in A \to (X \underset{˙}{\lor} p = Y \to (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y)))$
29	28	reximdvai	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X \underset{˙}{<} Y) \to (\exists p \in A X \underset{˙}{\lor} p = Y \to \exists p \in A (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y))$
30	29	expimpd	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y) \to \exists p \in A (\neg p \leq_{K} X \land X \underset{˙}{\lor} p = Y))$
31	30 8	sylibrd	$⊢ (K \in HL \land X \in B \land Y \in B) \to ((X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y) \to X C Y)$
32	14 31	impbid	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{<} Y \land \exists p \in A X \underset{˙}{\lor} p = Y))$

Metamath Proof Explorer

Theorem cvrval4N

Proof