Step | Hyp | Ref
| Expression |
1 | | lbsext.k |
. . . 4
⊢ (𝜑 → 𝒫 𝑉 ∈ dom
card) |
2 | | lbsext.s |
. . . . 5
⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} |
3 | 2 | ssrab3 3995 |
. . . 4
⊢ 𝑆 ⊆ 𝒫 𝑉 |
4 | | ssnum 9653 |
. . . 4
⊢
((𝒫 𝑉 ∈
dom card ∧ 𝑆 ⊆
𝒫 𝑉) → 𝑆 ∈ dom
card) |
5 | 1, 3, 4 | sylancl 589 |
. . 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
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) |
12 | 6, 7, 8, 9, 10, 11, 2 | lbsextlem1 20195 |
. . 3
⊢ (𝜑 → 𝑆 ≠ ∅) |
13 | 9 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → 𝑊 ∈ LVec) |
14 | 10 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → 𝐶 ⊆ 𝑉) |
15 | 11 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) |
16 | | eqid 2737 |
. . . . . 6
⊢
(LSubSp‘𝑊) =
(LSubSp‘𝑊) |
17 | | simpr1 1196 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → 𝑦 ⊆ 𝑆) |
18 | | simpr2 1197 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → 𝑦 ≠ ∅) |
19 | | simpr3 1198 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) →
[⊊] Or 𝑦) |
20 | | eqid 2737 |
. . . . . 6
⊢ ∪ 𝑢 ∈ 𝑦 (𝑁‘(𝑢 ∖ {𝑥})) = ∪
𝑢 ∈ 𝑦 (𝑁‘(𝑢 ∖ {𝑥})) |
21 | 6, 7, 8, 13, 14, 15, 2, 16, 17, 18, 19, 20 | lbsextlem3 20197 |
. . . . 5
⊢ ((𝜑 ∧ (𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦)) → ∪ 𝑦
∈ 𝑆) |
22 | 21 | ex 416 |
. . . 4
⊢ (𝜑 → ((𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∪ 𝑦
∈ 𝑆)) |
23 | 22 | alrimiv 1935 |
. . 3
⊢ (𝜑 → ∀𝑦((𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∪ 𝑦
∈ 𝑆)) |
24 | | zornn0g 10119 |
. . 3
⊢ ((𝑆 ∈ dom card ∧ 𝑆 ≠ ∅ ∧
∀𝑦((𝑦 ⊆ 𝑆 ∧ 𝑦 ≠ ∅ ∧ [⊊] Or
𝑦) → ∪ 𝑦
∈ 𝑆)) →
∃𝑠 ∈ 𝑆 ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡) |
25 | 5, 12, 23, 24 | syl3anc 1373 |
. 2
⊢ (𝜑 → ∃𝑠 ∈ 𝑆 ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡) |
26 | | simprl 771 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑠 ∈ 𝑆) |
27 | | sseq2 3927 |
. . . . . . . 8
⊢ (𝑧 = 𝑠 → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ 𝑠)) |
28 | | difeq1 4030 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑠 → (𝑧 ∖ {𝑥}) = (𝑠 ∖ {𝑥})) |
29 | 28 | fveq2d 6721 |
. . . . . . . . . . 11
⊢ (𝑧 = 𝑠 → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘(𝑠 ∖ {𝑥}))) |
30 | 29 | eleq2d 2823 |
. . . . . . . . . 10
⊢ (𝑧 = 𝑠 → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
31 | 30 | notbid 321 |
. . . . . . . . 9
⊢ (𝑧 = 𝑠 → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
32 | 31 | raleqbi1dv 3317 |
. . . . . . . 8
⊢ (𝑧 = 𝑠 → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
33 | 27, 32 | anbi12d 634 |
. . . . . . 7
⊢ (𝑧 = 𝑠 → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))))) |
34 | 33, 2 | elrab2 3605 |
. . . . . 6
⊢ (𝑠 ∈ 𝑆 ↔ (𝑠 ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))))) |
35 | 26, 34 | sylib 221 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑠 ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))))) |
36 | 35 | simpld 498 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑠 ∈ 𝒫 𝑉) |
37 | 36 | elpwid 4524 |
. . 3
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑠 ⊆ 𝑉) |
38 | | lveclmod 20143 |
. . . . . . 7
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
39 | 9, 38 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ LMod) |
40 | 39 | adantr 484 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑊 ∈ LMod) |
41 | 6, 8 | lspssv 20020 |
. . . . 5
⊢ ((𝑊 ∈ LMod ∧ 𝑠 ⊆ 𝑉) → (𝑁‘𝑠) ⊆ 𝑉) |
42 | 40, 37, 41 | syl2anc 587 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑁‘𝑠) ⊆ 𝑉) |
43 | | ssun1 4086 |
. . . . . . . . 9
⊢ 𝑠 ⊆ (𝑠 ∪ {𝑤}) |
44 | 43 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑠 ⊆ (𝑠 ∪ {𝑤})) |
45 | | ssun2 4087 |
. . . . . . . . . . 11
⊢ {𝑤} ⊆ (𝑠 ∪ {𝑤}) |
46 | | vsnid 4578 |
. . . . . . . . . . 11
⊢ 𝑤 ∈ {𝑤} |
47 | 45, 46 | sselii 3897 |
. . . . . . . . . 10
⊢ 𝑤 ∈ (𝑠 ∪ {𝑤}) |
48 | 6, 8 | lspssid 20022 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑠 ⊆ 𝑉) → 𝑠 ⊆ (𝑁‘𝑠)) |
49 | 40, 37, 48 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑠 ⊆ (𝑁‘𝑠)) |
50 | 49 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑠 ⊆ (𝑁‘𝑠)) |
51 | | eldifn 4042 |
. . . . . . . . . . . 12
⊢ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) → ¬ 𝑤 ∈ (𝑁‘𝑠)) |
52 | 51 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ¬ 𝑤 ∈ (𝑁‘𝑠)) |
53 | 50, 52 | ssneldd 3904 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ¬ 𝑤 ∈ 𝑠) |
54 | | nelne1 3038 |
. . . . . . . . . 10
⊢ ((𝑤 ∈ (𝑠 ∪ {𝑤}) ∧ ¬ 𝑤 ∈ 𝑠) → (𝑠 ∪ {𝑤}) ≠ 𝑠) |
55 | 47, 53, 54 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑠 ∪ {𝑤}) ≠ 𝑠) |
56 | 55 | necomd 2996 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑠 ≠ (𝑠 ∪ {𝑤})) |
57 | | df-pss 3885 |
. . . . . . . 8
⊢ (𝑠 ⊊ (𝑠 ∪ {𝑤}) ↔ (𝑠 ⊆ (𝑠 ∪ {𝑤}) ∧ 𝑠 ≠ (𝑠 ∪ {𝑤}))) |
58 | 44, 56, 57 | sylanbrc 586 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑠 ⊊ (𝑠 ∪ {𝑤})) |
59 | | psseq2 4003 |
. . . . . . . . 9
⊢ (𝑡 = (𝑠 ∪ {𝑤}) → (𝑠 ⊊ 𝑡 ↔ 𝑠 ⊊ (𝑠 ∪ {𝑤}))) |
60 | 59 | notbid 321 |
. . . . . . . 8
⊢ (𝑡 = (𝑠 ∪ {𝑤}) → (¬ 𝑠 ⊊ 𝑡 ↔ ¬ 𝑠 ⊊ (𝑠 ∪ {𝑤}))) |
61 | | simplrr 778 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡) |
62 | 37 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑠 ⊆ 𝑉) |
63 | | eldifi 4041 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) → 𝑤 ∈ 𝑉) |
64 | 63 | adantl 485 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝑤 ∈ 𝑉) |
65 | 64 | snssd 4722 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → {𝑤} ⊆ 𝑉) |
66 | 62, 65 | unssd 4100 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑠 ∪ {𝑤}) ⊆ 𝑉) |
67 | 6 | fvexi 6731 |
. . . . . . . . . . 11
⊢ 𝑉 ∈ V |
68 | 67 | elpw2 5238 |
. . . . . . . . . 10
⊢ ((𝑠 ∪ {𝑤}) ∈ 𝒫 𝑉 ↔ (𝑠 ∪ {𝑤}) ⊆ 𝑉) |
69 | 66, 68 | sylibr 237 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑠 ∪ {𝑤}) ∈ 𝒫 𝑉) |
70 | 35 | simprd 499 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝐶 ⊆ 𝑠 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
71 | 70 | simpld 498 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝐶 ⊆ 𝑠) |
72 | 71 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝐶 ⊆ 𝑠) |
73 | 72, 43 | sstrdi 3913 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → 𝐶 ⊆ (𝑠 ∪ {𝑤})) |
74 | 9 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑊 ∈ LVec) |
75 | 37 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑠 ⊆ 𝑉) |
76 | 75 | ssdifssd 4057 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → (𝑠 ∖ {𝑥}) ⊆ 𝑉) |
77 | 64 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑤 ∈ 𝑉) |
78 | | simprrr 782 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
79 | | difundir 4195 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑠 ∪ {𝑤}) ∖ {𝑥}) = ((𝑠 ∖ {𝑥}) ∪ ({𝑤} ∖ {𝑥})) |
80 | | simprrl 781 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑥 ∈ 𝑠) |
81 | 53 | adantrr 717 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ¬ 𝑤 ∈ 𝑠) |
82 | | nelne2 3039 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ ((𝑥 ∈ 𝑠 ∧ ¬ 𝑤 ∈ 𝑠) → 𝑥 ≠ 𝑤) |
83 | 80, 81, 82 | syl2anc 587 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑥 ≠ 𝑤) |
84 | | nelsn 4581 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ≠ 𝑤 → ¬ 𝑥 ∈ {𝑤}) |
85 | 83, 84 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ¬ 𝑥 ∈ {𝑤}) |
86 | | disjsn 4627 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (({𝑤} ∩ {𝑥}) = ∅ ↔ ¬ 𝑥 ∈ {𝑤}) |
87 | 85, 86 | sylibr 237 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ({𝑤} ∩ {𝑥}) = ∅) |
88 | | disj3 4368 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (({𝑤} ∩ {𝑥}) = ∅ ↔ {𝑤} = ({𝑤} ∖ {𝑥})) |
89 | 87, 88 | sylib 221 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → {𝑤} = ({𝑤} ∖ {𝑥})) |
90 | 89 | uneq2d 4077 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ((𝑠 ∖ {𝑥}) ∪ {𝑤}) = ((𝑠 ∖ {𝑥}) ∪ ({𝑤} ∖ {𝑥}))) |
91 | 79, 90 | eqtr4id 2797 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ((𝑠 ∪ {𝑤}) ∖ {𝑥}) = ((𝑠 ∖ {𝑥}) ∪ {𝑤})) |
92 | 91 | fveq2d 6721 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) = (𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑤}))) |
93 | 78, 92 | eleqtrd 2840 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑥 ∈ (𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑤}))) |
94 | 70 | simprd 499 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))) |
95 | 94 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))) |
96 | | rsp 3127 |
. . . . . . . . . . . . . . . . . . 19
⊢
(∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})) → (𝑥 ∈ 𝑠 → ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥})))) |
97 | 95, 80, 96 | sylc 65 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))) |
98 | 93, 97 | eldifd 3877 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑥 ∈ ((𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑤})) ∖ (𝑁‘(𝑠 ∖ {𝑥})))) |
99 | 6, 16, 8 | lspsolv 20180 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑊 ∈ LVec ∧ ((𝑠 ∖ {𝑥}) ⊆ 𝑉 ∧ 𝑤 ∈ 𝑉 ∧ 𝑥 ∈ ((𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑤})) ∖ (𝑁‘(𝑠 ∖ {𝑥}))))) → 𝑤 ∈ (𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑥}))) |
100 | 74, 76, 77, 98, 99 | syl13anc 1374 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑤 ∈ (𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑥}))) |
101 | | undif1 4390 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑠 ∖ {𝑥}) ∪ {𝑥}) = (𝑠 ∪ {𝑥}) |
102 | 80 | snssd 4722 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → {𝑥} ⊆ 𝑠) |
103 | | ssequn2 4097 |
. . . . . . . . . . . . . . . . . . 19
⊢ ({𝑥} ⊆ 𝑠 ↔ (𝑠 ∪ {𝑥}) = 𝑠) |
104 | 102, 103 | sylib 221 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → (𝑠 ∪ {𝑥}) = 𝑠) |
105 | 101, 104 | syl5eq 2790 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → ((𝑠 ∖ {𝑥}) ∪ {𝑥}) = 𝑠) |
106 | 105 | fveq2d 6721 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → (𝑁‘((𝑠 ∖ {𝑥}) ∪ {𝑥})) = (𝑁‘𝑠)) |
107 | 100, 106 | eleqtrd 2840 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ (𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠)) ∧ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) → 𝑤 ∈ (𝑁‘𝑠)) |
108 | 107 | expr 460 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ((𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) → 𝑤 ∈ (𝑁‘𝑠))) |
109 | 52, 108 | mtod 201 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ¬ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
110 | | imnan 403 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ 𝑠 → ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) ↔ ¬ (𝑥 ∈ 𝑠 ∧ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
111 | 109, 110 | sylibr 237 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑥 ∈ 𝑠 → ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
112 | 111 | ralrimiv 3104 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
113 | | difssd 4047 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑠 ∖ {𝑤}) ⊆ 𝑠) |
114 | 6, 8 | lspss 20021 |
. . . . . . . . . . . . . . 15
⊢ ((𝑊 ∈ LMod ∧ 𝑠 ⊆ 𝑉 ∧ (𝑠 ∖ {𝑤}) ⊆ 𝑠) → (𝑁‘(𝑠 ∖ {𝑤})) ⊆ (𝑁‘𝑠)) |
115 | 40, 37, 113, 114 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑁‘(𝑠 ∖ {𝑤})) ⊆ (𝑁‘𝑠)) |
116 | 115 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑁‘(𝑠 ∖ {𝑤})) ⊆ (𝑁‘𝑠)) |
117 | 116, 52 | ssneldd 3904 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ¬ 𝑤 ∈ (𝑁‘(𝑠 ∖ {𝑤}))) |
118 | | vex 3412 |
. . . . . . . . . . . . 13
⊢ 𝑤 ∈ V |
119 | | id 22 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → 𝑥 = 𝑤) |
120 | | sneq 4551 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 = 𝑤 → {𝑥} = {𝑤}) |
121 | 120 | difeq2d 4037 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 = 𝑤 → ((𝑠 ∪ {𝑤}) ∖ {𝑥}) = ((𝑠 ∪ {𝑤}) ∖ {𝑤})) |
122 | | difun2 4395 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑠 ∪ {𝑤}) ∖ {𝑤}) = (𝑠 ∖ {𝑤}) |
123 | 121, 122 | eqtrdi 2794 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 = 𝑤 → ((𝑠 ∪ {𝑤}) ∖ {𝑥}) = (𝑠 ∖ {𝑤})) |
124 | 123 | fveq2d 6721 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑤 → (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) = (𝑁‘(𝑠 ∖ {𝑤}))) |
125 | 119, 124 | eleq12d 2832 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑤 → (𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) ↔ 𝑤 ∈ (𝑁‘(𝑠 ∖ {𝑤})))) |
126 | 125 | notbid 321 |
. . . . . . . . . . . . 13
⊢ (𝑥 = 𝑤 → (¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) ↔ ¬ 𝑤 ∈ (𝑁‘(𝑠 ∖ {𝑤})))) |
127 | 118, 126 | ralsn 4597 |
. . . . . . . . . . . 12
⊢
(∀𝑥 ∈
{𝑤} ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) ↔ ¬ 𝑤 ∈ (𝑁‘(𝑠 ∖ {𝑤}))) |
128 | 117, 127 | sylibr 237 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ∀𝑥 ∈ {𝑤} ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
129 | | ralun 4106 |
. . . . . . . . . . 11
⊢
((∀𝑥 ∈
𝑠 ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})) ∧ ∀𝑥 ∈ {𝑤} ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) → ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
130 | 112, 128,
129 | syl2anc 587 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
131 | 73, 130 | jca 515 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝐶 ⊆ (𝑠 ∪ {𝑤}) ∧ ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
132 | | sseq2 3927 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ (𝑠 ∪ {𝑤}))) |
133 | | difeq1 4030 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (𝑧 ∖ {𝑥}) = ((𝑠 ∪ {𝑤}) ∖ {𝑥})) |
134 | 133 | fveq2d 6721 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))) |
135 | 134 | eleq2d 2823 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
136 | 135 | notbid 321 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
137 | 136 | raleqbi1dv 3317 |
. . . . . . . . . . 11
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥})))) |
138 | 132, 137 | anbi12d 634 |
. . . . . . . . . 10
⊢ (𝑧 = (𝑠 ∪ {𝑤}) → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ (𝑠 ∪ {𝑤}) ∧ ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) |
139 | 138, 2 | elrab2 3605 |
. . . . . . . . 9
⊢ ((𝑠 ∪ {𝑤}) ∈ 𝑆 ↔ ((𝑠 ∪ {𝑤}) ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ (𝑠 ∪ {𝑤}) ∧ ∀𝑥 ∈ (𝑠 ∪ {𝑤}) ¬ 𝑥 ∈ (𝑁‘((𝑠 ∪ {𝑤}) ∖ {𝑥}))))) |
140 | 69, 131, 139 | sylanbrc 586 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → (𝑠 ∪ {𝑤}) ∈ 𝑆) |
141 | 60, 61, 140 | rspcdva 3539 |
. . . . . . 7
⊢ (((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) ∧ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) → ¬ 𝑠 ⊊ (𝑠 ∪ {𝑤})) |
142 | 58, 141 | pm2.65da 817 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → ¬ 𝑤 ∈ (𝑉 ∖ (𝑁‘𝑠))) |
143 | 142 | eq0rdv 4319 |
. . . . 5
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑉 ∖ (𝑁‘𝑠)) = ∅) |
144 | | ssdif0 4278 |
. . . . 5
⊢ (𝑉 ⊆ (𝑁‘𝑠) ↔ (𝑉 ∖ (𝑁‘𝑠)) = ∅) |
145 | 143, 144 | sylibr 237 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑉 ⊆ (𝑁‘𝑠)) |
146 | 42, 145 | eqssd 3918 |
. . 3
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑁‘𝑠) = 𝑉) |
147 | 9 | adantr 484 |
. . . 4
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑊 ∈ LVec) |
148 | 6, 7, 8 | islbs2 20191 |
. . . 4
⊢ (𝑊 ∈ LVec → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝑉 ∧ (𝑁‘𝑠) = 𝑉 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))))) |
149 | 147, 148 | syl 17 |
. . 3
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → (𝑠 ∈ 𝐽 ↔ (𝑠 ⊆ 𝑉 ∧ (𝑁‘𝑠) = 𝑉 ∧ ∀𝑥 ∈ 𝑠 ¬ 𝑥 ∈ (𝑁‘(𝑠 ∖ {𝑥}))))) |
150 | 37, 146, 94, 149 | mpbir3and 1344 |
. 2
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ ∀𝑡 ∈ 𝑆 ¬ 𝑠 ⊊ 𝑡)) → 𝑠 ∈ 𝐽) |
151 | 25, 150, 71 | reximssdv 3195 |
1
⊢ (𝜑 → ∃𝑠 ∈ 𝐽 𝐶 ⊆ 𝑠) |