Theorem 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={\mathrm{Base}}_K$$
	cvrletr.l	$$⊢\underset{\dot{}}{\le }={\le }_K$$
	cvrletr.s	$$⊢\underset{\dot{}}{<}={<}_K$$
	cvrletr.c	$$⊢C={⋖}_K$$
Assertion	cvrval2	$$⊢\left(K\in A\wedge X\in B\wedge Y\in B\right)\to \left(XCY\leftrightarrow \left(X\underset{\dot{}}{<}Y\wedge \forall z\in B\left(\left(X\underset{\dot{}}{<}z\wedge z\underset{\dot{}}{\le }Y\right)\to z=Y\right)\right)\right)$$

Proof

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