cvrval3

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

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

Proof

Step	Hyp	Ref	Expression
1		cvrval3.b	$⊢ B = {Base}_{K}$
2		cvrval3.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrval3.j	$⊢ \underset{˙}{\lor} = join (K)$
4		cvrval3.c	$⊢ C = ⋖_{K}$
5		cvrval3.a	$⊢ A = Atoms (K)$
6		eqid	$⊢ <_{K} = <_{K}$
7	1 6 4	cvrlt	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to X <_{K} Y$
8	1 2 6 3 4 5	hlrelat3	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X <_{K} Y) \to \exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
9	7 8	syldan	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to \exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)$
10		simp3l	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X C (X \underset{˙}{\lor} p)$
11		simp1l1	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to K \in HL$
12		simp1l2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X \in B$
13		simp2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to p \in A$
14	1 2 3 4 5	cvr1	$⊢ (K \in HL \land X \in B \land p \in A) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
15	11 12 13 14	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
16	10 15	mpbird	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to \neg p \underset{˙}{\leq} X$
17	11	hllatd	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to K \in Lat$
18	1 5	atbase	$⊢ p \in A \to p \in B$
19	18	3ad2ant2	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to p \in B$
20	1 3	latjcl	$⊢ (K \in Lat \land X \in B \land p \in B) \to X \underset{˙}{\lor} p \in B$
21	17 12 19 20	syl3anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X \underset{˙}{\lor} p \in B$
22	1 6 4	cvrlt	$⊢ ((K \in HL \land X \in B \land X \underset{˙}{\lor} p \in B) \land X C (X \underset{˙}{\lor} p)) \to X <_{K} (X \underset{˙}{\lor} p)$
23	11 12 21 10 22	syl31anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X <_{K} (X \underset{˙}{\lor} p)$
24		simp3r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y$
25		hlpos	$⊢ K \in HL \to K \in Poset$
26	11 25	syl	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to K \in Poset$
27		simp1l3	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to Y \in B$
28		simp1r	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X C Y$
29	1 2 6 4	cvrnbtwn2	$⊢ (K \in Poset \land (X \in B \land Y \in B \land X \underset{˙}{\lor} p \in B) \land X C Y) \to ((X <_{K} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y) \leftrightarrow X \underset{˙}{\lor} p = Y)$
30	26 12 27 21 28 29	syl131anc	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to ((X <_{K} (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y) \leftrightarrow X \underset{˙}{\lor} p = Y)$
31	23 24 30	mpbi2and	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to X \underset{˙}{\lor} p = Y$
32	16 31	jca	$⊢ (((K \in HL \land X \in B \land Y \in B) \land X C Y) \land p \in A \land (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y)) \to (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)$
33	32	3exp	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (p \in A \to ((X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y) \to (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)))$
34	33	reximdvai	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to (\exists p \in A (X C (X \underset{˙}{\lor} p) \land (X \underset{˙}{\lor} p) \underset{˙}{\leq} Y) \to \exists p \in A (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y))$
35	9 34	mpd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land X C Y) \to \exists p \in A (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)$
36	35	ex	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \to \exists p \in A (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y))$
37		simp3l	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to \neg p \underset{˙}{\leq} X$
38		simp11	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to K \in HL$
39		simp12	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to X \in B$
40		simp2	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to p \in A$
41	38 39 40 14	syl3anc	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to (\neg p \underset{˙}{\leq} X \leftrightarrow X C (X \underset{˙}{\lor} p))$
42	37 41	mpbid	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to X C (X \underset{˙}{\lor} p)$
43		simp3r	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to X \underset{˙}{\lor} p = Y$
44	42 43	breqtrd	$⊢ ((K \in HL \land X \in B \land Y \in B) \land p \in A \land (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y)) \to X C Y$
45	44	rexlimdv3a	$⊢ (K \in HL \land X \in B \land Y \in B) \to (\exists p \in A (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y) \to X C Y)$
46	36 45	impbid	$⊢ (K \in HL \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \exists p \in A (\neg p \underset{˙}{\leq} X \land X \underset{˙}{\lor} p = Y))$

Metamath Proof Explorer

Theorem cvrval3

Proof