Metamath Proof Explorer

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 ⊢ ( 𝜑 → ∃ 𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠 )