cvrval

Description: Binary relation expressing B covers A , which means that B is larger than A and there is nothing in between. Definition 3.2.18 of PtakPulmannova p. 68. ( cvbr analog.) (Contributed by NM, 18-Sep-2011)

	Ref	Expression
Hypotheses	cvrfval.b	$⊢ B = {Base}_{K}$
	cvrfval.s	$⊢ \underset{˙}{<} = <_{K}$
	cvrfval.c	$⊢ C = ⋖_{K}$
Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	$⊢ B = {Base}_{K}$
2		cvrfval.s	$⊢ \underset{˙}{<} = <_{K}$
3		cvrfval.c	$⊢ C = ⋖_{K}$
4	1 2 3	cvrfval	$⊢ K \in A \to C = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y))\}$
5		3anass	$⊢ ((x \in B \land y \in B) \land x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)) \leftrightarrow ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))$
6	5	opabbii	$⊢ \{⟨x, y⟩ \| ((x \in B \land y \in B) \land x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y))\} = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\}$
7	4 6	eqtrdi	$⊢ K \in A \to C = \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\}$
8	7	breqd	$⊢ K \in A \to (X C Y \leftrightarrow X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} Y)$
9	8	3ad2ant1	$⊢ (K \in A \land X \in B \land Y \in B) \to (X C Y \leftrightarrow X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} Y)$
10		df-br	$⊢ X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} Y \leftrightarrow ⟨X, Y⟩ \in \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\}$
11		breq1	$⊢ x = X \to (x \underset{˙}{<} y \leftrightarrow X \underset{˙}{<} y)$
12		breq1	$⊢ x = X \to (x \underset{˙}{<} z \leftrightarrow X \underset{˙}{<} z)$
13	12	anbi1d	$⊢ x = X \to ((x \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow (X \underset{˙}{<} z \land z \underset{˙}{<} y))$
14	13	rexbidv	$⊢ x = X \to (\exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y))$
15	14	notbid	$⊢ x = X \to (\neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y))$
16	11 15	anbi12d	$⊢ x = X \to ((x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)) \leftrightarrow (X \underset{˙}{<} y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y)))$
17		breq2	$⊢ y = Y \to (X \underset{˙}{<} y \leftrightarrow X \underset{˙}{<} Y)$
18		breq2	$⊢ y = Y \to (z \underset{˙}{<} y \leftrightarrow z \underset{˙}{<} Y)$
19	18	anbi2d	$⊢ y = Y \to ((X \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
20	19	rexbidv	$⊢ y = Y \to (\exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
21	20	notbid	$⊢ y = Y \to (\neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y) \leftrightarrow \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y))$
22	17 21	anbi12d	$⊢ y = Y \to ((X \underset{˙}{<} y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} y)) \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
23	16 22	opelopab2	$⊢ (X \in B \land Y \in B) \to (⟨X, Y⟩ \in \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
24	10 23	bitrid	$⊢ (X \in B \land Y \in B) \to (X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} Y \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
25	24	3adant1	$⊢ (K \in A \land X \in B \land Y \in B) \to (X \{⟨x, y⟩ \| ((x \in B \land y \in B) \land (x \underset{˙}{<} y \land \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y)))\} Y \leftrightarrow (X \underset{˙}{<} Y \land \neg \exists z \in B (X \underset{˙}{<} z \land z \underset{˙}{<} Y)))$
26	9 25	bitrd	$⊢ (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)))$

Metamath Proof Explorer

Theorem cvrval

Proof