cvrcon3b

Description: Contraposition law for the covers relation. ( cvcon3 analog.) (Contributed by NM, 4-Nov-2011)

	Ref	Expression
Hypotheses	cvrcon3b.b	$⊢ B = {Base}_{K}$
	cvrcon3b.o	$⊢ \underset{˙}{⊥} = oc (K)$
	cvrcon3b.c	$⊢ C = ⋖_{K}$
Assertion	cvrcon3b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (Y) C \underset{˙}{⊥} (X))$

Proof

Step	Hyp	Ref	Expression
1		cvrcon3b.b	$⊢ B = {Base}_{K}$
2		cvrcon3b.o	$⊢ \underset{˙}{⊥} = oc (K)$
3		cvrcon3b.c	$⊢ C = ⋖_{K}$
4		eqid	$⊢ <_{K} = <_{K}$
5	1 4 2	opltcon3b	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X <_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (X))$
6		simpl1	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to K \in OP$
7		simpl2	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to X \in B$
8		simpr	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to x \in B$
9	1 4 2	opltcon3b	$⊢ (K \in OP \land X \in B \land x \in B) \to (X <_{K} x \leftrightarrow \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X))$
10	6 7 8 9	syl3anc	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to (X <_{K} x \leftrightarrow \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X))$
11		simpl3	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to Y \in B$
12	1 4 2	opltcon3b	$⊢ (K \in OP \land x \in B \land Y \in B) \to (x <_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x))$
13	6 8 11 12	syl3anc	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to (x <_{K} Y \leftrightarrow \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x))$
14	10 13	anbi12d	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to ((X <_{K} x \land x <_{K} Y) \leftrightarrow (\underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X) \land \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x)))$
15	1 2	opoccl	$⊢ (K \in OP \land x \in B) \to \underset{˙}{⊥} (x) \in B$
16	15	3ad2antl1	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to \underset{˙}{⊥} (x) \in B$
17		breq2	$⊢ y = \underset{˙}{⊥} (x) \to (\underset{˙}{⊥} (Y) <_{K} y \leftrightarrow \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x))$
18		breq1	$⊢ y = \underset{˙}{⊥} (x) \to (y <_{K} \underset{˙}{⊥} (X) \leftrightarrow \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X))$
19	17 18	anbi12d	$⊢ y = \underset{˙}{⊥} (x) \to ((\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)) \leftrightarrow (\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x) \land \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X)))$
20	19	rspcev	$⊢ (\underset{˙}{⊥} (x) \in B \land (\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x) \land \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X))) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X))$
21	20	ex	$⊢ \underset{˙}{⊥} (x) \in B \to ((\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x) \land \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X)) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
22	16 21	syl	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to ((\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x) \land \underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X)) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
23	22	ancomsd	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to ((\underset{˙}{⊥} (x) <_{K} \underset{˙}{⊥} (X) \land \underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (x)) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
24	14 23	sylbid	$⊢ ((K \in OP \land X \in B \land Y \in B) \land x \in B) \to ((X <_{K} x \land x <_{K} Y) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
25	24	rexlimdva	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\exists x \in B (X <_{K} x \land x <_{K} Y) \to \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
26		simpl1	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to K \in OP$
27		simpl3	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to Y \in B$
28		simpr	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to y \in B$
29	1 4 2	opltcon1b	$⊢ (K \in OP \land Y \in B \land y \in B) \to (\underset{˙}{⊥} (Y) <_{K} y \leftrightarrow \underset{˙}{⊥} (y) <_{K} Y)$
30	26 27 28 29	syl3anc	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to (\underset{˙}{⊥} (Y) <_{K} y \leftrightarrow \underset{˙}{⊥} (y) <_{K} Y)$
31		simpl2	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to X \in B$
32	1 4 2	opltcon2b	$⊢ (K \in OP \land y \in B \land X \in B) \to (y <_{K} \underset{˙}{⊥} (X) \leftrightarrow X <_{K} \underset{˙}{⊥} (y))$
33	26 28 31 32	syl3anc	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to (y <_{K} \underset{˙}{⊥} (X) \leftrightarrow X <_{K} \underset{˙}{⊥} (y))$
34	30 33	anbi12d	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to ((\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)) \leftrightarrow (\underset{˙}{⊥} (y) <_{K} Y \land X <_{K} \underset{˙}{⊥} (y)))$
35	1 2	opoccl	$⊢ (K \in OP \land y \in B) \to \underset{˙}{⊥} (y) \in B$
36	35	3ad2antl1	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to \underset{˙}{⊥} (y) \in B$
37		breq2	$⊢ x = \underset{˙}{⊥} (y) \to (X <_{K} x \leftrightarrow X <_{K} \underset{˙}{⊥} (y))$
38		breq1	$⊢ x = \underset{˙}{⊥} (y) \to (x <_{K} Y \leftrightarrow \underset{˙}{⊥} (y) <_{K} Y)$
39	37 38	anbi12d	$⊢ x = \underset{˙}{⊥} (y) \to ((X <_{K} x \land x <_{K} Y) \leftrightarrow (X <_{K} \underset{˙}{⊥} (y) \land \underset{˙}{⊥} (y) <_{K} Y))$
40	39	rspcev	$⊢ (\underset{˙}{⊥} (y) \in B \land (X <_{K} \underset{˙}{⊥} (y) \land \underset{˙}{⊥} (y) <_{K} Y)) \to \exists x \in B (X <_{K} x \land x <_{K} Y)$
41	40	ex	$⊢ \underset{˙}{⊥} (y) \in B \to ((X <_{K} \underset{˙}{⊥} (y) \land \underset{˙}{⊥} (y) <_{K} Y) \to \exists x \in B (X <_{K} x \land x <_{K} Y))$
42	36 41	syl	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to ((X <_{K} \underset{˙}{⊥} (y) \land \underset{˙}{⊥} (y) <_{K} Y) \to \exists x \in B (X <_{K} x \land x <_{K} Y))$
43	42	ancomsd	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to ((\underset{˙}{⊥} (y) <_{K} Y \land X <_{K} \underset{˙}{⊥} (y)) \to \exists x \in B (X <_{K} x \land x <_{K} Y))$
44	34 43	sylbid	$⊢ ((K \in OP \land X \in B \land Y \in B) \land y \in B) \to ((\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)) \to \exists x \in B (X <_{K} x \land x <_{K} Y))$
45	44	rexlimdva	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)) \to \exists x \in B (X <_{K} x \land x <_{K} Y))$
46	25 45	impbid	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\exists x \in B (X <_{K} x \land x <_{K} Y) \leftrightarrow \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
47	46	notbid	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\neg \exists x \in B (X <_{K} x \land x <_{K} Y) \leftrightarrow \neg \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X)))$
48	5 47	anbi12d	$⊢ (K \in OP \land X \in B \land Y \in B) \to ((X <_{K} Y \land \neg \exists x \in B (X <_{K} x \land x <_{K} Y)) \leftrightarrow (\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (X) \land \neg \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X))))$
49	1 4 3	cvrval	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X C Y \leftrightarrow (X <_{K} Y \land \neg \exists x \in B (X <_{K} x \land x <_{K} Y)))$
50		simp1	$⊢ (K \in OP \land X \in B \land Y \in B) \to K \in OP$
51	1 2	opoccl	$⊢ (K \in OP \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
52	51	3adant2	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (Y) \in B$
53	1 2	opoccl	$⊢ (K \in OP \land X \in B) \to \underset{˙}{⊥} (X) \in B$
54	53	3adant3	$⊢ (K \in OP \land X \in B \land Y \in B) \to \underset{˙}{⊥} (X) \in B$
55	1 4 3	cvrval	$⊢ (K \in OP \land \underset{˙}{⊥} (Y) \in B \land \underset{˙}{⊥} (X) \in B) \to (\underset{˙}{⊥} (Y) C \underset{˙}{⊥} (X) \leftrightarrow (\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (X) \land \neg \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X))))$
56	50 52 54 55	syl3anc	$⊢ (K \in OP \land X \in B \land Y \in B) \to (\underset{˙}{⊥} (Y) C \underset{˙}{⊥} (X) \leftrightarrow (\underset{˙}{⊥} (Y) <_{K} \underset{˙}{⊥} (X) \land \neg \exists y \in B (\underset{˙}{⊥} (Y) <_{K} y \land y <_{K} \underset{˙}{⊥} (X))))$
57	48 49 56	3bitr4d	$⊢ (K \in OP \land X \in B \land Y \in B) \to (X C Y \leftrightarrow \underset{˙}{⊥} (Y) C \underset{˙}{⊥} (X))$

Metamath Proof Explorer

Theorem cvrcon3b

Proof