lbsextlem4

Description: Lemma for lbsext . lbsextlem3 satisfies the conditions for the application of Zorn's lemma zorn (thus invoking AC), and so there is a maximal linearly independent set extending C . Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Hypotheses	lbsext.v	$⊢ V = {Base}_{W}$
	lbsext.j	$⊢ J = LBasis (W)$
	lbsext.n	$⊢ N = LSpan (W)$
	lbsext.w	$⊢ φ \to W \in LVec$
	lbsext.c	$⊢ φ \to C \subseteq V$
	lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
	lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
	lbsext.k	$⊢ φ \to 𝒫 V \in dom card$
Assertion	lbsextlem4	$⊢ φ \to \exists s \in J C \subseteq s$

Proof

Step	Hyp	Ref	Expression
1		lbsext.v	$⊢ V = {Base}_{W}$
2		lbsext.j	$⊢ J = LBasis (W)$
3		lbsext.n	$⊢ N = LSpan (W)$
4		lbsext.w	$⊢ φ \to W \in LVec$
5		lbsext.c	$⊢ φ \to C \subseteq V$
6		lbsext.x	$⊢ φ \to \forall x \in C \neg x \in N (C ∖ \{x\})$
7		lbsext.s	$⊢ S = \{z \in 𝒫 V \| (C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\}))\}$
8		lbsext.k	$⊢ φ \to 𝒫 V \in dom card$
9	7	ssrab3	$⊢ S \subseteq 𝒫 V$
10		ssnum	$⊢ (𝒫 V \in dom card \land S \subseteq 𝒫 V) \to S \in dom card$
11	8 9 10	sylancl	$⊢ φ \to S \in dom card$
12	1 2 3 4 5 6 7	lbsextlem1	$⊢ φ \to S \neq \emptyset$
13	4	adantr	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to W \in LVec$
14	5	adantr	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to C \subseteq V$
15	6	adantr	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to \forall x \in C \neg x \in N (C ∖ \{x\})$
16		eqid	$⊢ LSubSp (W) = LSubSp (W)$
17		simpr1	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to y \subseteq S$
18		simpr2	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to y \neq \emptyset$
19		simpr3	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to [\subset] Or y$
20		eqid	$⊢ ⋃_{u \in y} N (u ∖ \{x\}) = ⋃_{u \in y} N (u ∖ \{x\})$
21	1 2 3 13 14 15 7 16 17 18 19 20	lbsextlem3	$⊢ (φ \land (y \subseteq S \land y \neq \emptyset \land [\subset] Or y)) \to ⋃ y \in S$
22	21	ex	$⊢ φ \to ((y \subseteq S \land y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in S)$
23	22	alrimiv	$⊢ φ \to \forall y ((y \subseteq S \land y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in S)$
24		zornn0g	$⊢ (S \in dom card \land S \neq \emptyset \land \forall y ((y \subseteq S \land y \neq \emptyset \land [\subset] Or y) \to ⋃ y \in S)) \to \exists s \in S \forall t \in S \neg s \subset t$
25	11 12 23 24	syl3anc	$⊢ φ \to \exists s \in S \forall t \in S \neg s \subset t$
26		simprl	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s \in S$
27		sseq2	$⊢ z = s \to (C \subseteq z \leftrightarrow C \subseteq s)$
28		difeq1	$⊢ z = s \to z ∖ \{x\} = s ∖ \{x\}$
29	28	fveq2d	$⊢ z = s \to N (z ∖ \{x\}) = N (s ∖ \{x\})$
30	29	eleq2d	$⊢ z = s \to (x \in N (z ∖ \{x\}) \leftrightarrow x \in N (s ∖ \{x\}))$
31	30	notbid	$⊢ z = s \to (\neg x \in N (z ∖ \{x\}) \leftrightarrow \neg x \in N (s ∖ \{x\}))$
32	31	raleqbi1dv	$⊢ z = s \to (\forall x \in z \neg x \in N (z ∖ \{x\}) \leftrightarrow \forall x \in s \neg x \in N (s ∖ \{x\}))$
33	27 32	anbi12d	$⊢ z = s \to ((C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \leftrightarrow (C \subseteq s \land \forall x \in s \neg x \in N (s ∖ \{x\})))$
34	33 7	elrab2	$⊢ s \in S \leftrightarrow (s \in 𝒫 V \land (C \subseteq s \land \forall x \in s \neg x \in N (s ∖ \{x\})))$
35	26 34	sylib	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to (s \in 𝒫 V \land (C \subseteq s \land \forall x \in s \neg x \in N (s ∖ \{x\})))$
36	35	simpld	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s \in 𝒫 V$
37	36	elpwid	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s \subseteq V$
38		lveclmod	$⊢ W \in LVec \to W \in LMod$
39	4 38	syl	$⊢ φ \to W \in LMod$
40	39	adantr	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to W \in LMod$
41	1 3	lspssv	$⊢ (W \in LMod \land s \subseteq V) \to N (s) \subseteq V$
42	40 37 41	syl2anc	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to N (s) \subseteq V$
43		ssun1	$⊢ s \subseteq s \cup \{w\}$
44	43	a1i	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \subseteq s \cup \{w\}$
45		ssun2	$⊢ \{w\} \subseteq s \cup \{w\}$
46		vsnid	$⊢ w \in \{w\}$
47	45 46	sselii	$⊢ w \in (s \cup \{w\})$
48	1 3	lspssid	$⊢ (W \in LMod \land s \subseteq V) \to s \subseteq N (s)$
49	40 37 48	syl2anc	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s \subseteq N (s)$
50	49	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \subseteq N (s)$
51		eldifn	$⊢ w \in (V ∖ N (s)) \to \neg w \in N (s)$
52	51	adantl	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \neg w \in N (s)$
53	50 52	ssneldd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \neg w \in s$
54		nelne1	$⊢ (w \in (s \cup \{w\}) \land \neg w \in s) \to s \cup \{w\} \neq s$
55	47 53 54	sylancr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \cup \{w\} \neq s$
56	55	necomd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \neq s \cup \{w\}$
57		df-pss	$⊢ s \subset s \cup \{w\} \leftrightarrow (s \subseteq s \cup \{w\} \land s \neq s \cup \{w\})$
58	44 56 57	sylanbrc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \subset s \cup \{w\}$
59		psseq2	$⊢ t = s \cup \{w\} \to (s \subset t \leftrightarrow s \subset s \cup \{w\})$
60	59	notbid	$⊢ t = s \cup \{w\} \to (\neg s \subset t \leftrightarrow \neg s \subset s \cup \{w\})$
61		simplrr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \forall t \in S \neg s \subset t$
62	37	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \subseteq V$
63		eldifi	$⊢ w \in (V ∖ N (s)) \to w \in V$
64	63	adantl	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to w \in V$
65	64	snssd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \{w\} \subseteq V$
66	62 65	unssd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \cup \{w\} \subseteq V$
67	1	fvexi	$⊢ V \in V$
68	67	elpw2	$⊢ s \cup \{w\} \in 𝒫 V \leftrightarrow s \cup \{w\} \subseteq V$
69	66 68	sylibr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \cup \{w\} \in 𝒫 V$
70	35	simprd	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to (C \subseteq s \land \forall x \in s \neg x \in N (s ∖ \{x\}))$
71	70	simpld	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to C \subseteq s$
72	71	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to C \subseteq s$
73	72 43	sstrdi	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to C \subseteq s \cup \{w\}$
74	4	ad2antrr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to W \in LVec$
75	37	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to s \subseteq V$
76	75	ssdifssd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to s ∖ \{x\} \subseteq V$
77	64	adantrr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to w \in V$
78		simprrr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to x \in N ((s \cup \{w\}) ∖ \{x\})$
79		simprrl	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to x \in s$
80	53	adantrr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \neg w \in s$
81		nelne2	$⊢ (x \in s \land \neg w \in s) \to x \neq w$
82	79 80 81	syl2anc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to x \neq w$
83		nelsn	$⊢ x \neq w \to \neg x \in \{w\}$
84	82 83	syl	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \neg x \in \{w\}$
85		disjsn	$⊢ \{w\} \cap \{x\} = \emptyset \leftrightarrow \neg x \in \{w\}$
86	84 85	sylibr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \{w\} \cap \{x\} = \emptyset$
87		disj3	$⊢ \{w\} \cap \{x\} = \emptyset \leftrightarrow \{w\} = \{w\} ∖ \{x\}$
88	86 87	sylib	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \{w\} = \{w\} ∖ \{x\}$
89	88	uneq2d	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to (s ∖ \{x\}) \cup \{w\} = (s ∖ \{x\}) \cup (\{w\} ∖ \{x\})$
90		difundir	$⊢ (s \cup \{w\}) ∖ \{x\} = (s ∖ \{x\}) \cup (\{w\} ∖ \{x\})$
91	89 90	syl6reqr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to (s \cup \{w\}) ∖ \{x\} = (s ∖ \{x\}) \cup \{w\}$
92	91	fveq2d	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to N ((s \cup \{w\}) ∖ \{x\}) = N ((s ∖ \{x\}) \cup \{w\})$
93	78 92	eleqtrd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to x \in N ((s ∖ \{x\}) \cup \{w\})$
94	70	simprd	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to \forall x \in s \neg x \in N (s ∖ \{x\})$
95	94	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \forall x \in s \neg x \in N (s ∖ \{x\})$
96		rsp	$⊢ \forall x \in s \neg x \in N (s ∖ \{x\}) \to (x \in s \to \neg x \in N (s ∖ \{x\}))$
97	95 79 96	sylc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \neg x \in N (s ∖ \{x\})$
98	93 97	eldifd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to x \in (N ((s ∖ \{x\}) \cup \{w\}) ∖ N (s ∖ \{x\}))$
99	1 16 3	lspsolv	$⊢ (W \in LVec \land (s ∖ \{x\} \subseteq V \land w \in V \land x \in (N ((s ∖ \{x\}) \cup \{w\}) ∖ N (s ∖ \{x\})))) \to w \in N ((s ∖ \{x\}) \cup \{x\})$
100	74 76 77 98 99	syl13anc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to w \in N ((s ∖ \{x\}) \cup \{x\})$
101		undif1	$⊢ (s ∖ \{x\}) \cup \{x\} = s \cup \{x\}$
102	79	snssd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to \{x\} \subseteq s$
103		ssequn2	$⊢ \{x\} \subseteq s \leftrightarrow s \cup \{x\} = s$
104	102 103	sylib	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to s \cup \{x\} = s$
105	101 104	syl5eq	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to (s ∖ \{x\}) \cup \{x\} = s$
106	105	fveq2d	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to N ((s ∖ \{x\}) \cup \{x\}) = N (s)$
107	100 106	eleqtrd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land (w \in (V ∖ N (s)) \land (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})))) \to w \in N (s)$
108	107	expr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to ((x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\})) \to w \in N (s))$
109	52 108	mtod	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \neg (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\}))$
110		imnan	$⊢ (x \in s \to \neg x \in N ((s \cup \{w\}) ∖ \{x\})) \leftrightarrow \neg (x \in s \land x \in N ((s \cup \{w\}) ∖ \{x\}))$
111	109 110	sylibr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to (x \in s \to \neg x \in N ((s \cup \{w\}) ∖ \{x\}))$
112	111	ralrimiv	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \forall x \in s \neg x \in N ((s \cup \{w\}) ∖ \{x\})$
113		difssd	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s ∖ \{w\} \subseteq s$
114	1 3	lspss	$⊢ (W \in LMod \land s \subseteq V \land s ∖ \{w\} \subseteq s) \to N (s ∖ \{w\}) \subseteq N (s)$
115	40 37 113 114	syl3anc	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to N (s ∖ \{w\}) \subseteq N (s)$
116	115	adantr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to N (s ∖ \{w\}) \subseteq N (s)$
117	116 52	ssneldd	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \neg w \in N (s ∖ \{w\})$
118		vex	$⊢ w \in V$
119		id	$⊢ x = w \to x = w$
120		sneq	$⊢ x = w \to \{x\} = \{w\}$
121	120	difeq2d	$⊢ x = w \to (s \cup \{w\}) ∖ \{x\} = (s \cup \{w\}) ∖ \{w\}$
122		difun2	$⊢ (s \cup \{w\}) ∖ \{w\} = s ∖ \{w\}$
123	121 122	syl6eq	$⊢ x = w \to (s \cup \{w\}) ∖ \{x\} = s ∖ \{w\}$
124	123	fveq2d	$⊢ x = w \to N ((s \cup \{w\}) ∖ \{x\}) = N (s ∖ \{w\})$
125	119 124	eleq12d	$⊢ x = w \to (x \in N ((s \cup \{w\}) ∖ \{x\}) \leftrightarrow w \in N (s ∖ \{w\}))$
126	125	notbid	$⊢ x = w \to (\neg x \in N ((s \cup \{w\}) ∖ \{x\}) \leftrightarrow \neg w \in N (s ∖ \{w\}))$
127	118 126	ralsn	$⊢ \forall x \in \{w\} \neg x \in N ((s \cup \{w\}) ∖ \{x\}) \leftrightarrow \neg w \in N (s ∖ \{w\})$
128	117 127	sylibr	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \forall x \in \{w\} \neg x \in N ((s \cup \{w\}) ∖ \{x\})$
129		ralun	$⊢ (\forall x \in s \neg x \in N ((s \cup \{w\}) ∖ \{x\}) \land \forall x \in \{w\} \neg x \in N ((s \cup \{w\}) ∖ \{x\})) \to \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\})$
130	112 128 129	syl2anc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\})$
131	73 130	jca	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to (C \subseteq s \cup \{w\} \land \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\}))$
132		sseq2	$⊢ z = s \cup \{w\} \to (C \subseteq z \leftrightarrow C \subseteq s \cup \{w\})$
133		difeq1	$⊢ z = s \cup \{w\} \to z ∖ \{x\} = (s \cup \{w\}) ∖ \{x\}$
134	133	fveq2d	$⊢ z = s \cup \{w\} \to N (z ∖ \{x\}) = N ((s \cup \{w\}) ∖ \{x\})$
135	134	eleq2d	$⊢ z = s \cup \{w\} \to (x \in N (z ∖ \{x\}) \leftrightarrow x \in N ((s \cup \{w\}) ∖ \{x\}))$
136	135	notbid	$⊢ z = s \cup \{w\} \to (\neg x \in N (z ∖ \{x\}) \leftrightarrow \neg x \in N ((s \cup \{w\}) ∖ \{x\}))$
137	136	raleqbi1dv	$⊢ z = s \cup \{w\} \to (\forall x \in z \neg x \in N (z ∖ \{x\}) \leftrightarrow \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\}))$
138	132 137	anbi12d	$⊢ z = s \cup \{w\} \to ((C \subseteq z \land \forall x \in z \neg x \in N (z ∖ \{x\})) \leftrightarrow (C \subseteq s \cup \{w\} \land \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\})))$
139	138 7	elrab2	$⊢ s \cup \{w\} \in S \leftrightarrow (s \cup \{w\} \in 𝒫 V \land (C \subseteq s \cup \{w\} \land \forall x \in (s \cup \{w\}) \neg x \in N ((s \cup \{w\}) ∖ \{x\})))$
140	69 131 139	sylanbrc	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to s \cup \{w\} \in S$
141	60 61 140	rspcdva	$⊢ ((φ \land (s \in S \land \forall t \in S \neg s \subset t)) \land w \in (V ∖ N (s))) \to \neg s \subset s \cup \{w\}$
142	58 141	pm2.65da	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to \neg w \in (V ∖ N (s))$
143	142	eq0rdv	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to V ∖ N (s) = \emptyset$
144		ssdif0	$⊢ V \subseteq N (s) \leftrightarrow V ∖ N (s) = \emptyset$
145	143 144	sylibr	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to V \subseteq N (s)$
146	42 145	eqssd	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to N (s) = V$
147	4	adantr	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to W \in LVec$
148	1 2 3	islbs2	$⊢ W \in LVec \to (s \in J \leftrightarrow (s \subseteq V \land N (s) = V \land \forall x \in s \neg x \in N (s ∖ \{x\})))$
149	147 148	syl	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to (s \in J \leftrightarrow (s \subseteq V \land N (s) = V \land \forall x \in s \neg x \in N (s ∖ \{x\})))$
150	37 146 94 149	mpbir3and	$⊢ (φ \land (s \in S \land \forall t \in S \neg s \subset t)) \to s \in J$
151	25 150 71	reximssdv	$⊢ φ \to \exists s \in J C \subseteq s$

Metamath Proof Explorer

Theorem lbsextlem4

Proof