MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  lbsextlem4 Structured version   Visualization version   GIF version

Theorem lbsextlem4 20919
Description: Lemma for lbsext 20921. lbsextlem3 20918 satisfies the conditions for the application of Zorn's lemma zorn 10504 (thus invoking AC), and so there is a maximal linearly independent set extending 𝐢. Here we prove that such a set is a basis. (Contributed by Mario Carneiro, 25-Jun-2014.)
Hypotheses
Ref Expression
lbsext.v 𝑉 = (Baseβ€˜π‘Š)
lbsext.j 𝐽 = (LBasisβ€˜π‘Š)
lbsext.n 𝑁 = (LSpanβ€˜π‘Š)
lbsext.w (πœ‘ β†’ π‘Š ∈ LVec)
lbsext.c (πœ‘ β†’ 𝐢 βŠ† 𝑉)
lbsext.x (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐢 Β¬ π‘₯ ∈ (π‘β€˜(𝐢 βˆ– {π‘₯})))
lbsext.s 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐢 βŠ† 𝑧 ∧ βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})))}
lbsext.k (πœ‘ β†’ 𝒫 𝑉 ∈ dom card)
Assertion
Ref Expression
lbsextlem4 (πœ‘ β†’ βˆƒπ‘  ∈ 𝐽 𝐢 βŠ† 𝑠)
Distinct variable groups:   π‘₯,𝐽   πœ‘,π‘₯,𝑠   𝑆,𝑠,π‘₯   π‘₯,𝑧,𝐢   π‘₯,𝑁,𝑧   π‘₯,𝑉,𝑧   π‘₯,π‘Š   𝑧,𝑠   πœ‘,𝑠
Allowed substitution hints:   πœ‘(𝑧)   𝐢(𝑠)   𝑆(𝑧)   𝐽(𝑧,𝑠)   𝑁(𝑠)   𝑉(𝑠)   π‘Š(𝑧,𝑠)

Proof of Theorem lbsextlem4
Dummy variables 𝑒 𝑀 𝑦 𝑑 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 lbsext.k . . . 4 (πœ‘ β†’ 𝒫 𝑉 ∈ dom card)
2 lbsext.s . . . . 5 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐢 βŠ† 𝑧 ∧ βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})))}
32ssrab3 4079 . . . 4 𝑆 βŠ† 𝒫 𝑉
4 ssnum 10036 . . . 4 ((𝒫 𝑉 ∈ dom card ∧ 𝑆 βŠ† 𝒫 𝑉) β†’ 𝑆 ∈ dom card)
51, 3, 4sylancl 584 . . 3 (πœ‘ β†’ 𝑆 ∈ dom card)
6 lbsext.v . . . 4 𝑉 = (Baseβ€˜π‘Š)
7 lbsext.j . . . 4 𝐽 = (LBasisβ€˜π‘Š)
8 lbsext.n . . . 4 𝑁 = (LSpanβ€˜π‘Š)
9 lbsext.w . . . 4 (πœ‘ β†’ π‘Š ∈ LVec)
10 lbsext.c . . . 4 (πœ‘ β†’ 𝐢 βŠ† 𝑉)
11 lbsext.x . . . 4 (πœ‘ β†’ βˆ€π‘₯ ∈ 𝐢 Β¬ π‘₯ ∈ (π‘β€˜(𝐢 βˆ– {π‘₯})))
126, 7, 8, 9, 10, 11, 2lbsextlem1 20916 . . 3 (πœ‘ β†’ 𝑆 β‰  βˆ…)
139adantr 479 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ π‘Š ∈ LVec)
1410adantr 479 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ 𝐢 βŠ† 𝑉)
1511adantr 479 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ βˆ€π‘₯ ∈ 𝐢 Β¬ π‘₯ ∈ (π‘β€˜(𝐢 βˆ– {π‘₯})))
16 eqid 2730 . . . . . 6 (LSubSpβ€˜π‘Š) = (LSubSpβ€˜π‘Š)
17 simpr1 1192 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ 𝑦 βŠ† 𝑆)
18 simpr2 1193 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ 𝑦 β‰  βˆ…)
19 simpr3 1194 . . . . . 6 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ [⊊] Or 𝑦)
20 eqid 2730 . . . . . 6 βˆͺ 𝑒 ∈ 𝑦 (π‘β€˜(𝑒 βˆ– {π‘₯})) = βˆͺ 𝑒 ∈ 𝑦 (π‘β€˜(𝑒 βˆ– {π‘₯}))
216, 7, 8, 13, 14, 15, 2, 16, 17, 18, 19, 20lbsextlem3 20918 . . . . 5 ((πœ‘ ∧ (𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦)) β†’ βˆͺ 𝑦 ∈ 𝑆)
2221ex 411 . . . 4 (πœ‘ β†’ ((𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑆))
2322alrimiv 1928 . . 3 (πœ‘ β†’ βˆ€π‘¦((𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑆))
24 zornn0g 10502 . . 3 ((𝑆 ∈ dom card ∧ 𝑆 β‰  βˆ… ∧ βˆ€π‘¦((𝑦 βŠ† 𝑆 ∧ 𝑦 β‰  βˆ… ∧ [⊊] Or 𝑦) β†’ βˆͺ 𝑦 ∈ 𝑆)) β†’ βˆƒπ‘  ∈ 𝑆 βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)
255, 12, 23, 24syl3anc 1369 . 2 (πœ‘ β†’ βˆƒπ‘  ∈ 𝑆 βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)
26 simprl 767 . . . . . 6 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑠 ∈ 𝑆)
27 sseq2 4007 . . . . . . . 8 (𝑧 = 𝑠 β†’ (𝐢 βŠ† 𝑧 ↔ 𝐢 βŠ† 𝑠))
28 difeq1 4114 . . . . . . . . . . . 12 (𝑧 = 𝑠 β†’ (𝑧 βˆ– {π‘₯}) = (𝑠 βˆ– {π‘₯}))
2928fveq2d 6894 . . . . . . . . . . 11 (𝑧 = 𝑠 β†’ (π‘β€˜(𝑧 βˆ– {π‘₯})) = (π‘β€˜(𝑠 βˆ– {π‘₯})))
3029eleq2d 2817 . . . . . . . . . 10 (𝑧 = 𝑠 β†’ (π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯}))))
3130notbid 317 . . . . . . . . 9 (𝑧 = 𝑠 β†’ (Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯}))))
3231raleqbi1dv 3331 . . . . . . . 8 (𝑧 = 𝑠 β†’ (βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯}))))
3327, 32anbi12d 629 . . . . . . 7 (𝑧 = 𝑠 β†’ ((𝐢 βŠ† 𝑧 ∧ βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯}))) ↔ (𝐢 βŠ† 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))))
3433, 2elrab2 3685 . . . . . 6 (𝑠 ∈ 𝑆 ↔ (𝑠 ∈ 𝒫 𝑉 ∧ (𝐢 βŠ† 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))))
3526, 34sylib 217 . . . . 5 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (𝑠 ∈ 𝒫 𝑉 ∧ (𝐢 βŠ† 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))))
3635simpld 493 . . . 4 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑠 ∈ 𝒫 𝑉)
3736elpwid 4610 . . 3 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑠 βŠ† 𝑉)
38 lveclmod 20861 . . . . . . 7 (π‘Š ∈ LVec β†’ π‘Š ∈ LMod)
399, 38syl 17 . . . . . 6 (πœ‘ β†’ π‘Š ∈ LMod)
4039adantr 479 . . . . 5 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ π‘Š ∈ LMod)
416, 8lspssv 20738 . . . . 5 ((π‘Š ∈ LMod ∧ 𝑠 βŠ† 𝑉) β†’ (π‘β€˜π‘ ) βŠ† 𝑉)
4240, 37, 41syl2anc 582 . . . 4 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (π‘β€˜π‘ ) βŠ† 𝑉)
43 ssun1 4171 . . . . . . . . 9 𝑠 βŠ† (𝑠 βˆͺ {𝑀})
4443a1i 11 . . . . . . . 8 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑠 βŠ† (𝑠 βˆͺ {𝑀}))
45 ssun2 4172 . . . . . . . . . . 11 {𝑀} βŠ† (𝑠 βˆͺ {𝑀})
46 vsnid 4664 . . . . . . . . . . 11 𝑀 ∈ {𝑀}
4745, 46sselii 3978 . . . . . . . . . 10 𝑀 ∈ (𝑠 βˆͺ {𝑀})
486, 8lspssid 20740 . . . . . . . . . . . . 13 ((π‘Š ∈ LMod ∧ 𝑠 βŠ† 𝑉) β†’ 𝑠 βŠ† (π‘β€˜π‘ ))
4940, 37, 48syl2anc 582 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑠 βŠ† (π‘β€˜π‘ ))
5049adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑠 βŠ† (π‘β€˜π‘ ))
51 eldifn 4126 . . . . . . . . . . . 12 (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) β†’ Β¬ 𝑀 ∈ (π‘β€˜π‘ ))
5251adantl 480 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ Β¬ 𝑀 ∈ (π‘β€˜π‘ ))
5350, 52ssneldd 3984 . . . . . . . . . 10 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ Β¬ 𝑀 ∈ 𝑠)
54 nelne1 3037 . . . . . . . . . 10 ((𝑀 ∈ (𝑠 βˆͺ {𝑀}) ∧ Β¬ 𝑀 ∈ 𝑠) β†’ (𝑠 βˆͺ {𝑀}) β‰  𝑠)
5547, 53, 54sylancr 585 . . . . . . . . 9 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (𝑠 βˆͺ {𝑀}) β‰  𝑠)
5655necomd 2994 . . . . . . . 8 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑠 β‰  (𝑠 βˆͺ {𝑀}))
57 df-pss 3966 . . . . . . . 8 (𝑠 ⊊ (𝑠 βˆͺ {𝑀}) ↔ (𝑠 βŠ† (𝑠 βˆͺ {𝑀}) ∧ 𝑠 β‰  (𝑠 βˆͺ {𝑀})))
5844, 56, 57sylanbrc 581 . . . . . . 7 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑠 ⊊ (𝑠 βˆͺ {𝑀}))
59 psseq2 4087 . . . . . . . . 9 (𝑑 = (𝑠 βˆͺ {𝑀}) β†’ (𝑠 ⊊ 𝑑 ↔ 𝑠 ⊊ (𝑠 βˆͺ {𝑀})))
6059notbid 317 . . . . . . . 8 (𝑑 = (𝑠 βˆͺ {𝑀}) β†’ (Β¬ 𝑠 ⊊ 𝑑 ↔ Β¬ 𝑠 ⊊ (𝑠 βˆͺ {𝑀})))
61 simplrr 774 . . . . . . . 8 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)
6237adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑠 βŠ† 𝑉)
63 eldifi 4125 . . . . . . . . . . . . 13 (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) β†’ 𝑀 ∈ 𝑉)
6463adantl 480 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝑀 ∈ 𝑉)
6564snssd 4811 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ {𝑀} βŠ† 𝑉)
6662, 65unssd 4185 . . . . . . . . . 10 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (𝑠 βˆͺ {𝑀}) βŠ† 𝑉)
676fvexi 6904 . . . . . . . . . . 11 𝑉 ∈ V
6867elpw2 5344 . . . . . . . . . 10 ((𝑠 βˆͺ {𝑀}) ∈ 𝒫 𝑉 ↔ (𝑠 βˆͺ {𝑀}) βŠ† 𝑉)
6966, 68sylibr 233 . . . . . . . . 9 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (𝑠 βˆͺ {𝑀}) ∈ 𝒫 𝑉)
7035simprd 494 . . . . . . . . . . . . 13 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (𝐢 βŠ† 𝑠 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯}))))
7170simpld 493 . . . . . . . . . . . 12 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝐢 βŠ† 𝑠)
7271adantr 479 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝐢 βŠ† 𝑠)
7372, 43sstrdi 3993 . . . . . . . . . 10 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ 𝐢 βŠ† (𝑠 βˆͺ {𝑀}))
749ad2antrr 722 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘Š ∈ LVec)
7537adantr 479 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ 𝑠 βŠ† 𝑉)
7675ssdifssd 4141 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ (𝑠 βˆ– {π‘₯}) βŠ† 𝑉)
7764adantrr 713 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ 𝑀 ∈ 𝑉)
78 simprrr 778 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
79 difundir 4279 . . . . . . . . . . . . . . . . . . . . 21 ((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}) = ((𝑠 βˆ– {π‘₯}) βˆͺ ({𝑀} βˆ– {π‘₯}))
80 simprrl 777 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘₯ ∈ 𝑠)
8153adantrr 713 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ Β¬ 𝑀 ∈ 𝑠)
82 nelne2 3038 . . . . . . . . . . . . . . . . . . . . . . . . . 26 ((π‘₯ ∈ 𝑠 ∧ Β¬ 𝑀 ∈ 𝑠) β†’ π‘₯ β‰  𝑀)
8380, 81, 82syl2anc 582 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘₯ β‰  𝑀)
84 nelsn 4667 . . . . . . . . . . . . . . . . . . . . . . . . 25 (π‘₯ β‰  𝑀 β†’ Β¬ π‘₯ ∈ {𝑀})
8583, 84syl 17 . . . . . . . . . . . . . . . . . . . . . . . 24 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ Β¬ π‘₯ ∈ {𝑀})
86 disjsn 4714 . . . . . . . . . . . . . . . . . . . . . . . 24 (({𝑀} ∩ {π‘₯}) = βˆ… ↔ Β¬ π‘₯ ∈ {𝑀})
8785, 86sylibr 233 . . . . . . . . . . . . . . . . . . . . . . 23 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ ({𝑀} ∩ {π‘₯}) = βˆ…)
88 disj3 4452 . . . . . . . . . . . . . . . . . . . . . . 23 (({𝑀} ∩ {π‘₯}) = βˆ… ↔ {𝑀} = ({𝑀} βˆ– {π‘₯}))
8987, 88sylib 217 . . . . . . . . . . . . . . . . . . . . . 22 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ {𝑀} = ({𝑀} βˆ– {π‘₯}))
9089uneq2d 4162 . . . . . . . . . . . . . . . . . . . . 21 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ ((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀}) = ((𝑠 βˆ– {π‘₯}) βˆͺ ({𝑀} βˆ– {π‘₯})))
9179, 90eqtr4id 2789 . . . . . . . . . . . . . . . . . . . 20 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ ((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}) = ((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀}))
9291fveq2d 6894 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) = (π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀})))
9378, 92eleqtrd 2833 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘₯ ∈ (π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀})))
9470simprd 494 . . . . . . . . . . . . . . . . . . . 20 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))
9594adantr 479 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))
96 rsp 3242 . . . . . . . . . . . . . . . . . . 19 (βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})) β†’ (π‘₯ ∈ 𝑠 β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯}))))
9795, 80, 96sylc 65 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))
9893, 97eldifd 3958 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ π‘₯ ∈ ((π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀})) βˆ– (π‘β€˜(𝑠 βˆ– {π‘₯}))))
996, 16, 8lspsolv 20901 . . . . . . . . . . . . . . . . 17 ((π‘Š ∈ LVec ∧ ((𝑠 βˆ– {π‘₯}) βŠ† 𝑉 ∧ 𝑀 ∈ 𝑉 ∧ π‘₯ ∈ ((π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {𝑀})) βˆ– (π‘β€˜(𝑠 βˆ– {π‘₯}))))) β†’ 𝑀 ∈ (π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {π‘₯})))
10074, 76, 77, 98, 99syl13anc 1370 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ 𝑀 ∈ (π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {π‘₯})))
101 undif1 4474 . . . . . . . . . . . . . . . . . 18 ((𝑠 βˆ– {π‘₯}) βˆͺ {π‘₯}) = (𝑠 βˆͺ {π‘₯})
10280snssd 4811 . . . . . . . . . . . . . . . . . . 19 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ {π‘₯} βŠ† 𝑠)
103 ssequn2 4182 . . . . . . . . . . . . . . . . . . 19 ({π‘₯} βŠ† 𝑠 ↔ (𝑠 βˆͺ {π‘₯}) = 𝑠)
104102, 103sylib 217 . . . . . . . . . . . . . . . . . 18 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ (𝑠 βˆͺ {π‘₯}) = 𝑠)
105101, 104eqtrid 2782 . . . . . . . . . . . . . . . . 17 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ ((𝑠 βˆ– {π‘₯}) βˆͺ {π‘₯}) = 𝑠)
106105fveq2d 6894 . . . . . . . . . . . . . . . 16 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ (π‘β€˜((𝑠 βˆ– {π‘₯}) βˆͺ {π‘₯})) = (π‘β€˜π‘ ))
107100, 106eleqtrd 2833 . . . . . . . . . . . . . . 15 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ (𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )) ∧ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))) β†’ 𝑀 ∈ (π‘β€˜π‘ ))
108107expr 455 . . . . . . . . . . . . . 14 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ ((π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))) β†’ 𝑀 ∈ (π‘β€˜π‘ )))
10952, 108mtod 197 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ Β¬ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
110 imnan 398 . . . . . . . . . . . . 13 ((π‘₯ ∈ 𝑠 β†’ Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))) ↔ Β¬ (π‘₯ ∈ 𝑠 ∧ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
111109, 110sylibr 233 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (π‘₯ ∈ 𝑠 β†’ Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
112111ralrimiv 3143 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
113 difssd 4131 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (𝑠 βˆ– {𝑀}) βŠ† 𝑠)
1146, 8lspss 20739 . . . . . . . . . . . . . . 15 ((π‘Š ∈ LMod ∧ 𝑠 βŠ† 𝑉 ∧ (𝑠 βˆ– {𝑀}) βŠ† 𝑠) β†’ (π‘β€˜(𝑠 βˆ– {𝑀})) βŠ† (π‘β€˜π‘ ))
11540, 37, 113, 114syl3anc 1369 . . . . . . . . . . . . . 14 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (π‘β€˜(𝑠 βˆ– {𝑀})) βŠ† (π‘β€˜π‘ ))
116115adantr 479 . . . . . . . . . . . . 13 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (π‘β€˜(𝑠 βˆ– {𝑀})) βŠ† (π‘β€˜π‘ ))
117116, 52ssneldd 3984 . . . . . . . . . . . 12 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ Β¬ 𝑀 ∈ (π‘β€˜(𝑠 βˆ– {𝑀})))
118 vex 3476 . . . . . . . . . . . . 13 𝑀 ∈ V
119 id 22 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑀 β†’ π‘₯ = 𝑀)
120 sneq 4637 . . . . . . . . . . . . . . . . . 18 (π‘₯ = 𝑀 β†’ {π‘₯} = {𝑀})
121120difeq2d 4121 . . . . . . . . . . . . . . . . 17 (π‘₯ = 𝑀 β†’ ((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}) = ((𝑠 βˆͺ {𝑀}) βˆ– {𝑀}))
122 difun2 4479 . . . . . . . . . . . . . . . . 17 ((𝑠 βˆͺ {𝑀}) βˆ– {𝑀}) = (𝑠 βˆ– {𝑀})
123121, 122eqtrdi 2786 . . . . . . . . . . . . . . . 16 (π‘₯ = 𝑀 β†’ ((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}) = (𝑠 βˆ– {𝑀}))
124123fveq2d 6894 . . . . . . . . . . . . . . 15 (π‘₯ = 𝑀 β†’ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) = (π‘β€˜(𝑠 βˆ– {𝑀})))
125119, 124eleq12d 2825 . . . . . . . . . . . . . 14 (π‘₯ = 𝑀 β†’ (π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) ↔ 𝑀 ∈ (π‘β€˜(𝑠 βˆ– {𝑀}))))
126125notbid 317 . . . . . . . . . . . . 13 (π‘₯ = 𝑀 β†’ (Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) ↔ Β¬ 𝑀 ∈ (π‘β€˜(𝑠 βˆ– {𝑀}))))
127118, 126ralsn 4684 . . . . . . . . . . . 12 (βˆ€π‘₯ ∈ {𝑀} Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) ↔ Β¬ 𝑀 ∈ (π‘β€˜(𝑠 βˆ– {𝑀})))
128117, 127sylibr 233 . . . . . . . . . . 11 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ βˆ€π‘₯ ∈ {𝑀} Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
129 ralun 4191 . . . . . . . . . . 11 ((βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})) ∧ βˆ€π‘₯ ∈ {𝑀} Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))) β†’ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
130112, 128, 129syl2anc 582 . . . . . . . . . 10 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
13173, 130jca 510 . . . . . . . . 9 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (𝐢 βŠ† (𝑠 βˆͺ {𝑀}) ∧ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
132 sseq2 4007 . . . . . . . . . . 11 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (𝐢 βŠ† 𝑧 ↔ 𝐢 βŠ† (𝑠 βˆͺ {𝑀})))
133 difeq1 4114 . . . . . . . . . . . . . . 15 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (𝑧 βˆ– {π‘₯}) = ((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))
134133fveq2d 6894 . . . . . . . . . . . . . 14 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (π‘β€˜(𝑧 βˆ– {π‘₯})) = (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))
135134eleq2d 2817 . . . . . . . . . . . . 13 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
136135notbid 317 . . . . . . . . . . . 12 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
137136raleqbi1dv 3331 . . . . . . . . . . 11 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ (βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯})) ↔ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯}))))
138132, 137anbi12d 629 . . . . . . . . . 10 (𝑧 = (𝑠 βˆͺ {𝑀}) β†’ ((𝐢 βŠ† 𝑧 ∧ βˆ€π‘₯ ∈ 𝑧 Β¬ π‘₯ ∈ (π‘β€˜(𝑧 βˆ– {π‘₯}))) ↔ (𝐢 βŠ† (𝑠 βˆͺ {𝑀}) ∧ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))))
139138, 2elrab2 3685 . . . . . . . . 9 ((𝑠 βˆͺ {𝑀}) ∈ 𝑆 ↔ ((𝑠 βˆͺ {𝑀}) ∈ 𝒫 𝑉 ∧ (𝐢 βŠ† (𝑠 βˆͺ {𝑀}) ∧ βˆ€π‘₯ ∈ (𝑠 βˆͺ {𝑀}) Β¬ π‘₯ ∈ (π‘β€˜((𝑠 βˆͺ {𝑀}) βˆ– {π‘₯})))))
14069, 131, 139sylanbrc 581 . . . . . . . 8 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ (𝑠 βˆͺ {𝑀}) ∈ 𝑆)
14160, 61, 140rspcdva 3612 . . . . . . 7 (((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) ∧ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ ))) β†’ Β¬ 𝑠 ⊊ (𝑠 βˆͺ {𝑀}))
14258, 141pm2.65da 813 . . . . . 6 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ Β¬ 𝑀 ∈ (𝑉 βˆ– (π‘β€˜π‘ )))
143142eq0rdv 4403 . . . . 5 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (𝑉 βˆ– (π‘β€˜π‘ )) = βˆ…)
144 ssdif0 4362 . . . . 5 (𝑉 βŠ† (π‘β€˜π‘ ) ↔ (𝑉 βˆ– (π‘β€˜π‘ )) = βˆ…)
145143, 144sylibr 233 . . . 4 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑉 βŠ† (π‘β€˜π‘ ))
14642, 145eqssd 3998 . . 3 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (π‘β€˜π‘ ) = 𝑉)
1479adantr 479 . . . 4 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ π‘Š ∈ LVec)
1486, 7, 8islbs2 20912 . . . 4 (π‘Š ∈ LVec β†’ (𝑠 ∈ 𝐽 ↔ (𝑠 βŠ† 𝑉 ∧ (π‘β€˜π‘ ) = 𝑉 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))))
149147, 148syl 17 . . 3 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ (𝑠 ∈ 𝐽 ↔ (𝑠 βŠ† 𝑉 ∧ (π‘β€˜π‘ ) = 𝑉 ∧ βˆ€π‘₯ ∈ 𝑠 Β¬ π‘₯ ∈ (π‘β€˜(𝑠 βˆ– {π‘₯})))))
15037, 146, 94, 149mpbir3and 1340 . 2 ((πœ‘ ∧ (𝑠 ∈ 𝑆 ∧ βˆ€π‘‘ ∈ 𝑆 Β¬ 𝑠 ⊊ 𝑑)) β†’ 𝑠 ∈ 𝐽)
15125, 150, 71reximssdv 3170 1 (πœ‘ β†’ βˆƒπ‘  ∈ 𝐽 𝐢 βŠ† 𝑠)
Colors of variables: wff setvar class
Syntax hints:  Β¬ wn 3   β†’ wi 4   ↔ wb 205   ∧ wa 394   ∧ w3a 1085  βˆ€wal 1537   = wceq 1539   ∈ wcel 2104   β‰  wne 2938  βˆ€wral 3059  βˆƒwrex 3068  {crab 3430   βˆ– cdif 3944   βˆͺ cun 3945   ∩ cin 3946   βŠ† wss 3947   ⊊ wpss 3948  βˆ…c0 4321  π’« cpw 4601  {csn 4627  βˆͺ cuni 4907  βˆͺ ciun 4996   Or wor 5586  dom cdm 5675  β€˜cfv 6542   [⊊] crpss 7714  cardccrd 9932  Basecbs 17148  LModclmod 20614  LSubSpclss 20686  LSpanclspn 20726  LBasisclbs 20829  LVecclvec 20857
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-rep 5284  ax-sep 5298  ax-nul 5305  ax-pow 5362  ax-pr 5426  ax-un 7727  ax-cnex 11168  ax-resscn 11169  ax-1cn 11170  ax-icn 11171  ax-addcl 11172  ax-addrcl 11173  ax-mulcl 11174  ax-mulrcl 11175  ax-mulcom 11176  ax-addass 11177  ax-mulass 11178  ax-distr 11179  ax-i2m1 11180  ax-1ne0 11181  ax-1rid 11182  ax-rnegex 11183  ax-rrecex 11184  ax-cnre 11185  ax-pre-lttri 11186  ax-pre-lttrn 11187  ax-pre-ltadd 11188  ax-pre-mulgt0 11189
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3or 1086  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ne 2939  df-nel 3045  df-ral 3060  df-rex 3069  df-rmo 3374  df-reu 3375  df-rab 3431  df-v 3474  df-sbc 3777  df-csb 3893  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-pss 3966  df-nul 4322  df-if 4528  df-pw 4603  df-sn 4628  df-pr 4630  df-op 4634  df-uni 4908  df-int 4950  df-iun 4998  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5573  df-eprel 5579  df-po 5587  df-so 5588  df-fr 5630  df-se 5631  df-we 5632  df-xp 5681  df-rel 5682  df-cnv 5683  df-co 5684  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-pred 6299  df-ord 6366  df-on 6367  df-lim 6368  df-suc 6369  df-iota 6494  df-fun 6544  df-fn 6545  df-f 6546  df-f1 6547  df-fo 6548  df-f1o 6549  df-fv 6550  df-isom 6551  df-riota 7367  df-ov 7414  df-oprab 7415  df-mpo 7416  df-rpss 7715  df-om 7858  df-1st 7977  df-2nd 7978  df-tpos 8213  df-frecs 8268  df-wrecs 8299  df-recs 8373  df-rdg 8412  df-1o 8468  df-oadd 8472  df-er 8705  df-en 8942  df-dom 8943  df-sdom 8944  df-fin 8945  df-dju 9898  df-card 9936  df-pnf 11254  df-mnf 11255  df-xr 11256  df-ltxr 11257  df-le 11258  df-sub 11450  df-neg 11451  df-nn 12217  df-2 12279  df-3 12280  df-sets 17101  df-slot 17119  df-ndx 17131  df-base 17149  df-ress 17178  df-plusg 17214  df-mulr 17215  df-0g 17391  df-mgm 18565  df-sgrp 18644  df-mnd 18660  df-grp 18858  df-minusg 18859  df-sbg 18860  df-cmn 19691  df-abl 19692  df-mgp 20029  df-rng 20047  df-ur 20076  df-ring 20129  df-oppr 20225  df-dvdsr 20248  df-unit 20249  df-invr 20279  df-drng 20502  df-lmod 20616  df-lss 20687  df-lsp 20727  df-lbs 20830  df-lvec 20858
This theorem is referenced by:  lbsextg  20920
  Copyright terms: Public domain W3C validator