cvrval2

Description: Binary relation expressing Y covers X . Definition of covers in Kalmbach p. 15. ( cvbr2 analog.) (Contributed by NM, 16-Nov-2011)

	Ref	Expression
Hypotheses	cvrletr.b	$⊢ B = {Base}_{K}$
	cvrletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
	cvrletr.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrletr.c	$⊢ C = ⋖_{K}$
Assertion	cvrval2	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{<} Y \land \forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y)))$

Proof

Step	Hyp	Ref	Expression
1		cvrletr.b	$⊢ B = {Base}_{K}$
2		cvrletr.l	$⊢ \underset{˙}{\leq} = \leq_{K}$
3		cvrletr.s	$⊢ \underset{˙}{<} = <_{K}$
4		cvrletr.c	$⊢ C = ⋖_{K}$
5	1 3 4	cvrval	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
6		iman	$⊢ ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y) \leftrightarrow \neg ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land \neg z = Y)$
7		df-ne	$⊢ z \neq Y \leftrightarrow \neg z = Y$
8	7	anbi2i	$⊢ ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land z \neq Y) \leftrightarrow ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land \neg z = Y)$
9	6 8	xchbinxr	$⊢ ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y) \leftrightarrow \neg ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land z \neq Y)$
10		anass	$⊢ ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land z \neq Y) \leftrightarrow (X \underset{˙}{<} z \land (z \underset{˙}{\leq} Y \land z \neq Y))$
11	2 3	pltval	$⊢ (K \in A \land z \in B \land Y \in B) \to (z \underset{˙}{<} Y \leftrightarrow (z \underset{˙}{\leq} Y \land z \neq Y))$
12	11	3com23	$⊢ (K \in A \land Y \in B \land z \in B) \to (z \underset{˙}{<} Y \leftrightarrow (z \underset{˙}{\leq} Y \land z \neq Y))$
13	12	3expa	$⊢ ((K \in A \land Y \in B) \land z \in B) \to (z \underset{˙}{<} Y \leftrightarrow (z \underset{˙}{\leq} Y \land z \neq Y))$
14	13	anbi2d	$⊢ ((K \in A \land Y \in B) \land z \in B) \to ((X \underset{˙}{<} z \land z \underset{˙}{<} Y) \leftrightarrow (X \underset{˙}{<} z \land (z \underset{˙}{\leq} Y \land z \neq Y)))$
15	10 14	bitr4id	$⊢ ((K \in A \land Y \in B) \land z \in B) \to (((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land z \neq Y) \leftrightarrow (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
16	15	notbid	$⊢ ((K \in A \land Y \in B) \land z \in B) \to (\neg ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \land z \neq Y) \leftrightarrow \neg (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
17	9 16	syl5bb	$⊢ ((K \in A \land Y \in B) \land z \in B) \to (((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y) \leftrightarrow \neg (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
18	17	ralbidva	$⊢ (K \in A \land Y \in B) \to (\forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y) \leftrightarrow \forall z \in B \neg (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
19		ralnex	$⊢ \forall z \in B \neg (X \underset{˙}{<} z \land z \underset{˙}{<} Y) \leftrightarrow \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)$
20	18 19	bitrdi	$⊢ (K \in A \land Y \in B) \to (\forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y) \leftrightarrow \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
21	20	anbi2d	$⊢ (K \in A \land Y \in B) \to ((X \underset{˙}{<} Y \land \forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y)) \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
22	21	3adant2	$⊢ (K \in A \land X \in B \land Y \in B) \to ((X \underset{˙}{<} Y \land \forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y)) \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
23	5 22	bitr4d	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X \underset{˙}{<} Y \land \forall z \in B ((X \underset{˙}{<} z \land z \underset{˙}{\leq} Y) \to z = Y)))$

Metamath Proof Explorer

Theorem cvrval2

Proof