This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem lspexchn2

Description: Exchange property for span of a pair with negated membership. TODO: look at uses of lspexch to see if this will shorten proofs. (Contributed by NM, 24-May-2015)

		Ref	Expression
	Hypotheses	lspexchn2.v	$⊢ V = {Base}_{W}$
		lspexchn2.n	$⊢ N = LSpan (W)$
		lspexchn2.w	$⊢ φ \to W \in LVec$
		lspexchn2.x	$⊢ φ \to X \in V$
		lspexchn2.y	$⊢ φ \to Y \in V$
		lspexchn2.z	$⊢ φ \to Z \in V$
		lspexchn2.q	$⊢ φ \to \neg Y \in N (\{Z\})$
		lspexchn2.e	$⊢ φ \to \neg X \in N (\{Z, Y\})$
	Assertion	lspexchn2	$⊢ φ \to \neg Y \in N (\{Z, X\})$

Proof

Step	Hyp	Ref	Expression
1		lspexchn2.v	$⊢ V = {Base}_{W}$
2		lspexchn2.n	$⊢ N = LSpan (W)$
3		lspexchn2.w	$⊢ φ \to W \in LVec$
4		lspexchn2.x	$⊢ φ \to X \in V$
5		lspexchn2.y	$⊢ φ \to Y \in V$
6		lspexchn2.z	$⊢ φ \to Z \in V$
7		lspexchn2.q	$⊢ φ \to \neg Y \in N (\{Z\})$
8		lspexchn2.e	$⊢ φ \to \neg X \in N (\{Z, Y\})$
9		prcom	$⊢ \{Z, Y\} = \{Y, Z\}$
10	9	fveq2i	$⊢ N (\{Z, Y\}) = N (\{Y, Z\})$
11	10	eleq2i	$⊢ X \in N (\{Z, Y\}) \leftrightarrow X \in N (\{Y, Z\})$
12	8 11	sylnib	$⊢ φ \to \neg X \in N (\{Y, Z\})$
13	1 2 3 4 5 6 7 12	lspexchn1	$⊢ φ \to \neg Y \in N (\{X, Z\})$
14		prcom	$⊢ \{X, Z\} = \{Z, X\}$
15	14	fveq2i	$⊢ N (\{X, Z\}) = N (\{Z, X\})$
16	15	eleq2i	$⊢ Y \in N (\{X, Z\}) \leftrightarrow Y \in N (\{Z, X\})$
17	13 16	sylnib	$⊢ φ \to \neg Y \in N (\{Z, X\})$