Theorem 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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lbsext.j	⊢ 𝐽 = ( LBasis ‘ 𝑊 )
	lbsext.n	⊢ 𝑁 = ( LSpan ‘ 𝑊 )
	lbsext.w	⊢ ( 𝜑 → 𝑊 ∈ LVec )
	lbsext.c	⊢ ( 𝜑 → 𝐶 ⊆ 𝑉 )
	lbsext.x	⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝐶 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝐶 ∖ { 𝑥 } ) ) )
	lbsext.s	⊢ 𝑆 = { 𝑧 ∈ 𝒫 𝑉 ∣ ( 𝐶 ⊆ 𝑧 ∧ ∀ 𝑥 ∈ 𝑧 ¬ 𝑥 ∈ ( 𝑁 ‘ ( 𝑧 ∖ { 𝑥 } ) ) ) }
	lbsext.k	⊢ ( 𝜑 → 𝒫 𝑉 ∈ dom card )
Assertion	lbsextlem4	⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠 )

Proof

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