dvh3dim3N

Description: There is a vector that is outside of 2 spans. TODO: decide to use either this or dvh3dim2 everywhere. If this one is needed, make dvh3dim2 into a lemma. (Contributed by NM, 21-May-2015) (New usage is discouraged.)

	Ref	Expression
Hypotheses	dvh3dim.h	$⊢ H = LHyp (K)$
	dvh3dim.u	$⊢ U = DVecH (K) (W)$
	dvh3dim.v	$⊢ V = {Base}_{U}$
	dvh3dim.n	$⊢ N = LSpan (U)$
	dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
	dvh3dim.x	$⊢ φ \to X \in V$
	dvh3dim.y	$⊢ φ \to Y \in V$
	dvh3dim2.z	$⊢ φ \to Z \in V$
	dvh3dim3.t	$⊢ φ \to T \in V$
Assertion	dvh3dim3N	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$

Proof

Step	Hyp	Ref	Expression
1		dvh3dim.h	$⊢ H = LHyp (K)$
2		dvh3dim.u	$⊢ U = DVecH (K) (W)$
3		dvh3dim.v	$⊢ V = {Base}_{U}$
4		dvh3dim.n	$⊢ N = LSpan (U)$
5		dvh3dim.k	$⊢ φ \to (K \in HL \land W \in H)$
6		dvh3dim.x	$⊢ φ \to X \in V$
7		dvh3dim.y	$⊢ φ \to Y \in V$
8		dvh3dim2.z	$⊢ φ \to Z \in V$
9		dvh3dim3.t	$⊢ φ \to T \in V$
10		eqid	$⊢ LSubSp (U) = LSubSp (U)$
11	1 2 5	dvhlmod	$⊢ φ \to U \in LMod$
12	11	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to U \in LMod$
13	3 10 4 11 8 9	lspprcl	$⊢ φ \to N (\{Z, T\}) \in LSubSp (U)$
14	13	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to N (\{Z, T\}) \in LSubSp (U)$
15		simpr	$⊢ (φ \land Y \in N (\{Z, T\})) \to Y \in N (\{Z, T\})$
16	3 4 11 8 9	lspprid2	$⊢ φ \to T \in N (\{Z, T\})$
17	16	adantr	$⊢ (φ \land Y \in N (\{Z, T\})) \to T \in N (\{Z, T\})$
18	10 4 12 14 15 17	lspprss	$⊢ (φ \land Y \in N (\{Z, T\})) \to N (\{Y, T\}) \subseteq N (\{Z, T\})$
19		sspss	$⊢ N (\{Y, T\}) \subseteq N (\{Z, T\}) \leftrightarrow (N (\{Y, T\}) \subset N (\{Z, T\}) \lor N (\{Y, T\}) = N (\{Z, T\}))$
20	18 19	sylib	$⊢ (φ \land Y \in N (\{Z, T\})) \to (N (\{Y, T\}) \subset N (\{Z, T\}) \lor N (\{Y, T\}) = N (\{Z, T\}))$
21	1 2 5	dvhlvec	$⊢ φ \to U \in LVec$
22	21	adantr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to U \in LVec$
23	3 10 4 11 7 9	lspprcl	$⊢ φ \to N (\{Y, T\}) \in LSubSp (U)$
24	23	adantr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to N (\{Y, T\}) \in LSubSp (U)$
25	8	adantr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to Z \in V$
26	9	adantr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to T \in V$
27		simpr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to N (\{Y, T\}) \subset N (\{Z, T\})$
28	3 10 4 22 24 25 26 27	lspprat	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to \exists w \in V N (\{Y, T\}) = N (\{w\})$
29	5	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to (K \in HL \land W \in H)$
30		simp2	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to w \in V$
31	6	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to X \in V$
32	8	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to Z \in V$
33	1 2 3 4 29 30 31 32	dvh3dim2	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to \exists z \in V (\neg z \in N (\{w, X\}) \land \neg z \in N (\{w, Z\}))$
34	11	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to U \in LMod$
35	10	lsssssubg	$⊢ U \in LMod \to LSubSp (U) \subseteq SubGrp (U)$
36	34 35	syl	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to LSubSp (U) \subseteq SubGrp (U)$
37	3 10 4	lspsncl	$⊢ (U \in LMod \land X \in V) \to N (\{X\}) \in LSubSp (U)$
38	11 6 37	syl2anc	$⊢ φ \to N (\{X\}) \in LSubSp (U)$
39	38	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X\}) \in LSubSp (U)$
40	36 39	sseldd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X\}) \in SubGrp (U)$
41	3 10 4	lspsncl	$⊢ (U \in LMod \land w \in V) \to N (\{w\}) \in LSubSp (U)$
42	34 30 41	syl2anc	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{w\}) \in LSubSp (U)$
43	36 42	sseldd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{w\}) \in SubGrp (U)$
44		prssi	$⊢ (Y \in V \land T \in V) \to \{Y, T\} \subseteq V$
45	7 9 44	syl2anc	$⊢ φ \to \{Y, T\} \subseteq V$
46		snsspr1	$⊢ \{Y\} \subseteq \{Y, T\}$
47	46	a1i	$⊢ φ \to \{Y\} \subseteq \{Y, T\}$
48	3 4	lspss	$⊢ (U \in LMod \land \{Y, T\} \subseteq V \land \{Y\} \subseteq \{Y, T\}) \to N (\{Y\}) \subseteq N (\{Y, T\})$
49	11 45 47 48	syl3anc	$⊢ φ \to N (\{Y\}) \subseteq N (\{Y, T\})$
50	49	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Y\}) \subseteq N (\{Y, T\})$
51		simp3	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Y, T\}) = N (\{w\})$
52	50 51	sseqtrd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Y\}) \subseteq N (\{w\})$
53		eqid	$⊢ LSSum (U) = LSSum (U)$
54	53	lsmless2	$⊢ (N (\{X\}) \in SubGrp (U) \land N (\{w\}) \in SubGrp (U) \land N (\{Y\}) \subseteq N (\{w\})) \to N (\{X\}) LSSum (U) N (\{Y\}) \subseteq N (\{X\}) LSSum (U) N (\{w\})$
55	40 43 52 54	syl3anc	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X\}) LSSum (U) N (\{Y\}) \subseteq N (\{X\}) LSSum (U) N (\{w\})$
56	3 4 53 11 6 7	lsmpr	$⊢ φ \to N (\{X, Y\}) = N (\{X\}) LSSum (U) N (\{Y\})$
57	56	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X, Y\}) = N (\{X\}) LSSum (U) N (\{Y\})$
58		prcom	$⊢ \{w, X\} = \{X, w\}$
59	58	fveq2i	$⊢ N (\{w, X\}) = N (\{X, w\})$
60	3 4 53 34 31 30	lsmpr	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X, w\}) = N (\{X\}) LSSum (U) N (\{w\})$
61	59 60	syl5eq	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{w, X\}) = N (\{X\}) LSSum (U) N (\{w\})$
62	55 57 61	3sstr4d	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{X, Y\}) \subseteq N (\{w, X\})$
63	62	ssneld	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to (\neg z \in N (\{w, X\}) \to \neg z \in N (\{X, Y\}))$
64	3 10 4	lspsncl	$⊢ (U \in LMod \land Z \in V) \to N (\{Z\}) \in LSubSp (U)$
65	11 8 64	syl2anc	$⊢ φ \to N (\{Z\}) \in LSubSp (U)$
66	65	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z\}) \in LSubSp (U)$
67	36 66	sseldd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z\}) \in SubGrp (U)$
68		snsspr2	$⊢ \{T\} \subseteq \{Y, T\}$
69	68	a1i	$⊢ φ \to \{T\} \subseteq \{Y, T\}$
70	3 4	lspss	$⊢ (U \in LMod \land \{Y, T\} \subseteq V \land \{T\} \subseteq \{Y, T\}) \to N (\{T\}) \subseteq N (\{Y, T\})$
71	11 45 69 70	syl3anc	$⊢ φ \to N (\{T\}) \subseteq N (\{Y, T\})$
72	71	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{T\}) \subseteq N (\{Y, T\})$
73	72 51	sseqtrd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{T\}) \subseteq N (\{w\})$
74	53	lsmless2	$⊢ (N (\{Z\}) \in SubGrp (U) \land N (\{w\}) \in SubGrp (U) \land N (\{T\}) \subseteq N (\{w\})) \to N (\{Z\}) LSSum (U) N (\{T\}) \subseteq N (\{Z\}) LSSum (U) N (\{w\})$
75	67 43 73 74	syl3anc	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z\}) LSSum (U) N (\{T\}) \subseteq N (\{Z\}) LSSum (U) N (\{w\})$
76	3 4 53 11 8 9	lsmpr	$⊢ φ \to N (\{Z, T\}) = N (\{Z\}) LSSum (U) N (\{T\})$
77	76	3ad2ant1	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z, T\}) = N (\{Z\}) LSSum (U) N (\{T\})$
78		prcom	$⊢ \{w, Z\} = \{Z, w\}$
79	78	fveq2i	$⊢ N (\{w, Z\}) = N (\{Z, w\})$
80	3 4 53 34 32 30	lsmpr	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z, w\}) = N (\{Z\}) LSSum (U) N (\{w\})$
81	79 80	syl5eq	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{w, Z\}) = N (\{Z\}) LSSum (U) N (\{w\})$
82	75 77 81	3sstr4d	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to N (\{Z, T\}) \subseteq N (\{w, Z\})$
83	82	ssneld	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to (\neg z \in N (\{w, Z\}) \to \neg z \in N (\{Z, T\}))$
84	63 83	anim12d	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to ((\neg z \in N (\{w, X\}) \land \neg z \in N (\{w, Z\})) \to (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
85	84	reximdv	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to (\exists z \in V (\neg z \in N (\{w, X\}) \land \neg z \in N (\{w, Z\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
86	33 85	mpd	$⊢ (φ \land w \in V \land N (\{Y, T\}) = N (\{w\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
87	86	rexlimdv3a	$⊢ φ \to (\exists w \in V N (\{Y, T\}) = N (\{w\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
88	87	adantr	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to (\exists w \in V N (\{Y, T\}) = N (\{w\}) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
89	28 88	mpd	$⊢ (φ \land N (\{Y, T\}) \subset N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
90	1 2 3 4 5 7 6 9	dvh3dim2	$⊢ φ \to \exists z \in V (\neg z \in N (\{Y, X\}) \land \neg z \in N (\{Y, T\}))$
91	90	adantr	$⊢ (φ \land N (\{Y, T\}) = N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{Y, X\}) \land \neg z \in N (\{Y, T\}))$
92		simpr	$⊢ (φ \land N (\{Y, T\}) = N (\{Z, T\})) \to N (\{Y, T\}) = N (\{Z, T\})$
93		prcom	$⊢ \{Y, X\} = \{X, Y\}$
94	93	fveq2i	$⊢ N (\{Y, X\}) = N (\{X, Y\})$
95	94	eleq2i	$⊢ z \in N (\{Y, X\}) \leftrightarrow z \in N (\{X, Y\})$
96	95	notbii	$⊢ \neg z \in N (\{Y, X\}) \leftrightarrow \neg z \in N (\{X, Y\})$
97	96	a1i	$⊢ N (\{Y, T\}) = N (\{Z, T\}) \to (\neg z \in N (\{Y, X\}) \leftrightarrow \neg z \in N (\{X, Y\}))$
98		eleq2	$⊢ N (\{Y, T\}) = N (\{Z, T\}) \to (z \in N (\{Y, T\}) \leftrightarrow z \in N (\{Z, T\}))$
99	98	notbid	$⊢ N (\{Y, T\}) = N (\{Z, T\}) \to (\neg z \in N (\{Y, T\}) \leftrightarrow \neg z \in N (\{Z, T\}))$
100	97 99	anbi12d	$⊢ N (\{Y, T\}) = N (\{Z, T\}) \to ((\neg z \in N (\{Y, X\}) \land \neg z \in N (\{Y, T\})) \leftrightarrow (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
101	92 100	syl	$⊢ (φ \land N (\{Y, T\}) = N (\{Z, T\})) \to ((\neg z \in N (\{Y, X\}) \land \neg z \in N (\{Y, T\})) \leftrightarrow (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
102	101	rexbidv	$⊢ (φ \land N (\{Y, T\}) = N (\{Z, T\})) \to (\exists z \in V (\neg z \in N (\{Y, X\}) \land \neg z \in N (\{Y, T\})) \leftrightarrow \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
103	91 102	mpbid	$⊢ (φ \land N (\{Y, T\}) = N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
104	89 103	jaodan	$⊢ (φ \land (N (\{Y, T\}) \subset N (\{Z, T\}) \lor N (\{Y, T\}) = N (\{Z, T\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
105	20 104	syldan	$⊢ (φ \land Y \in N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
106	1 2 3 4 5 7 6 9	dvh3dim2	$⊢ φ \to \exists w \in V (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))$
107	106	adantr	$⊢ (φ \land \neg Y \in N (\{Z, T\})) \to \exists w \in V (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))$
108		simpl1l	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to φ$
109	108 11	syl	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to U \in LMod$
110		simpl2	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to w \in V$
111	108 7	syl	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to Y \in V$
112		eqid	$⊢ +_{U} = +_{U}$
113	3 112	lmodvacl	$⊢ (U \in LMod \land w \in V \land Y \in V) \to w +_{U} Y \in V$
114	109 110 111 113	syl3anc	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to w +_{U} Y \in V$
115	3 10 4 11 6 7	lspprcl	$⊢ φ \to N (\{X, Y\}) \in LSubSp (U)$
116	108 115	syl	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to N (\{X, Y\}) \in LSubSp (U)$
117	3 4 11 6 7	lspprid2	$⊢ φ \to Y \in N (\{X, Y\})$
118	108 117	syl	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to Y \in N (\{X, Y\})$
119		simpl3l	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \neg w \in N (\{Y, X\})$
120	94	eleq2i	$⊢ w \in N (\{Y, X\}) \leftrightarrow w \in N (\{X, Y\})$
121	119 120	sylnib	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \neg w \in N (\{X, Y\})$
122	3 112 10 109 116 118 110 121	lssvancl2	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \neg w +_{U} Y \in N (\{X, Y\})$
123	108 13	syl	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to N (\{Z, T\}) \in LSubSp (U)$
124		simpr	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to w \in N (\{Z, T\})$
125		simpl1r	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \neg Y \in N (\{Z, T\})$
126	3 112 10 109 123 124 111 125	lssvancl1	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \neg w +_{U} Y \in N (\{Z, T\})$
127		eleq1	$⊢ z = w +_{U} Y \to (z \in N (\{X, Y\}) \leftrightarrow w +_{U} Y \in N (\{X, Y\}))$
128	127	notbid	$⊢ z = w +_{U} Y \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg w +_{U} Y \in N (\{X, Y\}))$
129		eleq1	$⊢ z = w +_{U} Y \to (z \in N (\{Z, T\}) \leftrightarrow w +_{U} Y \in N (\{Z, T\}))$
130	129	notbid	$⊢ z = w +_{U} Y \to (\neg z \in N (\{Z, T\}) \leftrightarrow \neg w +_{U} Y \in N (\{Z, T\}))$
131	128 130	anbi12d	$⊢ z = w +_{U} Y \to ((\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})) \leftrightarrow (\neg w +_{U} Y \in N (\{X, Y\}) \land \neg w +_{U} Y \in N (\{Z, T\})))$
132	131	rspcev	$⊢ (w +_{U} Y \in V \land (\neg w +_{U} Y \in N (\{X, Y\}) \land \neg w +_{U} Y \in N (\{Z, T\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
133	114 122 126 132	syl12anc	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land w \in N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
134		simpl2	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land \neg w \in N (\{Z, T\})) \to w \in V$
135		simpl3l	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land \neg w \in N (\{Z, T\})) \to \neg w \in N (\{Y, X\})$
136	135 120	sylnib	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land \neg w \in N (\{Z, T\})) \to \neg w \in N (\{X, Y\})$
137		simpr	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land \neg w \in N (\{Z, T\})) \to \neg w \in N (\{Z, T\})$
138		eleq1	$⊢ z = w \to (z \in N (\{X, Y\}) \leftrightarrow w \in N (\{X, Y\}))$
139	138	notbid	$⊢ z = w \to (\neg z \in N (\{X, Y\}) \leftrightarrow \neg w \in N (\{X, Y\}))$
140		eleq1	$⊢ z = w \to (z \in N (\{Z, T\}) \leftrightarrow w \in N (\{Z, T\}))$
141	140	notbid	$⊢ z = w \to (\neg z \in N (\{Z, T\}) \leftrightarrow \neg w \in N (\{Z, T\}))$
142	139 141	anbi12d	$⊢ z = w \to ((\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})) \leftrightarrow (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{Z, T\})))$
143	142	rspcev	$⊢ (w \in V \land (\neg w \in N (\{X, Y\}) \land \neg w \in N (\{Z, T\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
144	134 136 137 143	syl12anc	$⊢ (((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \land \neg w \in N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
145	133 144	pm2.61dan	$⊢ ((φ \land \neg Y \in N (\{Z, T\})) \land w \in V \land (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\}))) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
146	145	rexlimdv3a	$⊢ (φ \land \neg Y \in N (\{Z, T\})) \to (\exists w \in V (\neg w \in N (\{Y, X\}) \land \neg w \in N (\{Y, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\})))$
147	107 146	mpd	$⊢ (φ \land \neg Y \in N (\{Z, T\})) \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$
148	105 147	pm2.61dan	$⊢ φ \to \exists z \in V (\neg z \in N (\{X, Y\}) \land \neg z \in N (\{Z, T\}))$

Metamath Proof Explorer

Theorem dvh3dim3N

Proof