cvrfval

Description: Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011)

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

Proof

Step	Hyp	Ref	Expression
1		cvrfval.b	$⊢ B = {Base}_{K}$
2		cvrfval.s	$⊢ \underset{˙}{<} = <_{K}$
3		cvrfval.c	$⊢ C = ⋖_{K}$
4		elex	$⊢ K \in A \to K \in V$
5		fveq2	$⊢ p = K \to {Base}_{p} = {Base}_{K}$
6	5 1	syl6eqr	$⊢ p = K \to {Base}_{p} = B$
7	6	eleq2d	$⊢ p = K \to (x \in {Base}_{p} \leftrightarrow x \in B)$
8	6	eleq2d	$⊢ p = K \to (y \in {Base}_{p} \leftrightarrow y \in B)$
9	7 8	anbi12d	$⊢ p = K \to ((x \in {Base}_{p} \land y \in {Base}_{p}) \leftrightarrow (x \in B \land y \in B))$
10		fveq2	$⊢ p = K \to <_{p} = <_{K}$
11	10 2	syl6eqr	$⊢ p = K \to <_{p} = \underset{˙}{<}$
12	11	breqd	$⊢ p = K \to (x <_{p} y \leftrightarrow x \underset{˙}{<} y)$
13	11	breqd	$⊢ p = K \to (x <_{p} z \leftrightarrow x \underset{˙}{<} z)$
14	11	breqd	$⊢ p = K \to (z <_{p} y \leftrightarrow z \underset{˙}{<} y)$
15	13 14	anbi12d	$⊢ p = K \to ((x <_{p} z \land z <_{p} y) \leftrightarrow (x \underset{˙}{<} z \land z \underset{˙}{<} y))$
16	6 15	rexeqbidv	$⊢ p = K \to (\exists z \in {Base}_{p} (x <_{p} z \land z <_{p} y) \leftrightarrow \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y))$
17	16	notbid	$⊢ p = K \to (\neg \exists z \in {Base}_{p} (x <_{p} z \land z <_{p} y) \leftrightarrow \neg \exists z \in B (x \underset{˙}{<} z \land z \underset{˙}{<} y))$
18	9 12 17	3anbi123d	$⊢ p = K \to (((x \in {Base}_{p} \land y \in {Base}_{p}) \land x <_{p} y \land \neg \exists z \in {Base}_{p} (x <_{p} z \land z <_{p} 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)))$
19	18	opabbidv	$⊢ p = K \to \{⟨x, y⟩ \| ((x \in {Base}_{p} \land y \in {Base}_{p}) \land x <_{p} y \land \neg \exists z \in {Base}_{p} (x <_{p} z \land z <_{p} 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))\}$
20		df-covers	$⊢ ⋖ = (p \in V ⟼ \{⟨x, y⟩ \| ((x \in {Base}_{p} \land y \in {Base}_{p}) \land x <_{p} y \land \neg \exists z \in {Base}_{p} (x <_{p} z \land z <_{p} y))\})$
21		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)))$
22	21	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)))\}$
23	1	fvexi	$⊢ B \in V$
24	23 23	xpex	$⊢ B \times B \in V$
25		opabssxp	$⊢ \{⟨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)))\} \subseteq B \times B$
26	24 25	ssexi	$⊢ \{⟨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)))\} \in V$
27	22 26	eqeltri	$⊢ \{⟨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))\} \in V$
28	19 20 27	fvmpt	$⊢ K \in V \to ⋖_{K} = \{⟨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))\}$
29	3 28	syl5eq	$⊢ K \in V \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))\}$
30	4 29	syl	$⊢ 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))\}$

Metamath Proof Explorer

Theorem cvrfval

Proof