Step | Hyp | Ref
| Expression |
1 | | lbsext.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
2 | | lbsext.s |
. . . . . 6
⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} |
3 | 2 | ssrab3 3971 |
. . . . 5
⊢ 𝑆 ⊆ 𝒫 𝑉 |
4 | 1, 3 | sstrdi 3889 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉) |
5 | | sspwuni 4985 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝑉 ↔ ∪ 𝐴
⊆ 𝑉) |
6 | 4, 5 | sylib 221 |
. . 3
⊢ (𝜑 → ∪ 𝐴
⊆ 𝑉) |
7 | | lbsext.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
8 | 7 | fvexi 6688 |
. . . 4
⊢ 𝑉 ∈ V |
9 | 8 | elpw2 5213 |
. . 3
⊢ (∪ 𝐴
∈ 𝒫 𝑉 ↔
∪ 𝐴 ⊆ 𝑉) |
10 | 6, 9 | sylibr 237 |
. 2
⊢ (𝜑 → ∪ 𝐴
∈ 𝒫 𝑉) |
11 | | ssintub 4854 |
. . . . 5
⊢ 𝐶 ⊆ ∩ {𝑧
∈ 𝒫 𝑉 ∣
𝐶 ⊆ 𝑧} |
12 | | simpl 486 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶 ⊆ 𝑧) |
13 | 12 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝑉 → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶 ⊆ 𝑧)) |
14 | 13 | ss2rabi 3966 |
. . . . . . . 8
⊢ {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} |
15 | 2, 14 | eqsstri 3911 |
. . . . . . 7
⊢ 𝑆 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} |
16 | 1, 15 | sstrdi 3889 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧}) |
17 | | intss 4857 |
. . . . . 6
⊢ (𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} → ∩ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} ⊆ ∩ 𝐴) |
18 | 16, 17 | syl 17 |
. . . . 5
⊢ (𝜑 → ∩ {𝑧
∈ 𝒫 𝑉 ∣
𝐶 ⊆ 𝑧} ⊆ ∩ 𝐴) |
19 | 11, 18 | sstrid 3888 |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ ∩ 𝐴) |
20 | | lbsext.z |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ ∅) |
21 | | intssuni 4858 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
⊆ ∪ 𝐴) |
22 | 20, 21 | syl 17 |
. . . 4
⊢ (𝜑 → ∩ 𝐴
⊆ ∪ 𝐴) |
23 | 19, 22 | sstrd 3887 |
. . 3
⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴) |
24 | | eluni2 4800 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑦 ∈
𝐴 𝑥 ∈ 𝑦) |
25 | | simpll1 1213 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝜑) |
26 | | lbsext.w |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ LVec) |
27 | | lveclmod 19997 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
28 | 26, 27 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ LMod) |
29 | 25, 28 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑊 ∈ LMod) |
30 | 25, 1 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝐴 ⊆ 𝑆) |
31 | | lbsext.r |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → [⊊] Or 𝐴) |
32 | 25, 31 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → [⊊] Or 𝐴) |
33 | | simpll2 1214 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑦 ∈ 𝐴) |
34 | | simplr 769 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑢 ∈ 𝐴) |
35 | | sorpssun 7474 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑦 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → (𝑦 ∪ 𝑢) ∈ 𝐴) |
36 | 32, 33, 34, 35 | syl12anc 836 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝐴) |
37 | 30, 36 | sseldd 3878 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝑆) |
38 | 3, 37 | sseldi 3875 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝒫 𝑉) |
39 | 38 | elpwid 4499 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ⊆ 𝑉) |
40 | 39 | ssdifssd 4033 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ((𝑦 ∪ 𝑢) ∖ {𝑥}) ⊆ 𝑉) |
41 | | ssun2 4063 |
. . . . . . . . . . . 12
⊢ 𝑢 ⊆ (𝑦 ∪ 𝑢) |
42 | | ssdif 4030 |
. . . . . . . . . . . 12
⊢ (𝑢 ⊆ (𝑦 ∪ 𝑢) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
43 | 41, 42 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
44 | | lbsext.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (LSpan‘𝑊) |
45 | 7, 44 | lspss 19875 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ∪ 𝑢) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
46 | 29, 40, 43, 45 | syl3anc 1372 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
47 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
48 | 46, 47 | sseldd 3878 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
49 | | sseq2 3903 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ (𝑦 ∪ 𝑢))) |
50 | | difeq1 4006 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑧 ∖ {𝑥}) = ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
51 | 50 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
52 | 51 | eleq2d 2818 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
53 | 52 | notbid 321 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
54 | 53 | raleqbi1dv 3308 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
55 | 49, 54 | anbi12d 634 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑢) → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))))) |
56 | 55, 2 | elrab2 3591 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 ↔ ((𝑦 ∪ 𝑢) ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))))) |
57 | 56 | simprbi 500 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 → (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
58 | 57 | simprd 499 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 → ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
59 | 37, 58 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
60 | | simpll3 1215 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ 𝑦) |
61 | | elun1 4066 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑦 → 𝑥 ∈ (𝑦 ∪ 𝑢)) |
62 | 60, 61 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑦 ∪ 𝑢)) |
63 | | rsp 3118 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})) → (𝑥 ∈ (𝑦 ∪ 𝑢) → ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
64 | 59, 62, 63 | sylc 65 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
65 | 48, 64 | pm2.65da 817 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) → ¬ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
66 | 65 | nrexdv 3180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → ¬ ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
67 | | lbsext.j |
. . . . . . . . . . . . . . . 16
⊢ 𝐽 = (LBasis‘𝑊) |
68 | | lbsext.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ⊆ 𝑉) |
69 | | lbsext.x |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) |
70 | | lbsext.p |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = (LSubSp‘𝑊) |
71 | | lbsext.t |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) |
72 | 7, 67, 44, 26, 68, 69, 2, 70, 1, 20, 31, 71 | lbsextlem2 20050 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇)) |
73 | 72 | simpld 498 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ 𝑃) |
74 | 7, 70 | lssss 19827 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑃 → 𝑇 ⊆ 𝑉) |
75 | 73, 74 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ⊆ 𝑉) |
76 | 72 | simprd 499 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∪ 𝐴
∖ {𝑥}) ⊆ 𝑇) |
77 | 7, 44 | lspss 19875 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ (𝑁‘𝑇)) |
78 | 28, 75, 76, 77 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ (𝑁‘𝑇)) |
79 | 70, 44 | lspid 19873 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑃) → (𝑁‘𝑇) = 𝑇) |
80 | 28, 73, 79 | syl2anc 587 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘𝑇) = 𝑇) |
81 | 78, 80 | sseqtrd 3917 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ 𝑇) |
82 | 81 | 3ad2ant1 1134 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ 𝑇) |
83 | 82, 71 | sseqtrdi 3927 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
84 | 83 | sseld 3876 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})) → 𝑥 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})))) |
85 | | eliun 4885 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
86 | 84, 85 | syl6ib 254 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})) → ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
87 | 66, 86 | mtod 201 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
88 | 87 | rexlimdv3a 3196 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
89 | 24, 88 | syl5bi 245 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
90 | 89 | ralrimiv 3095 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
91 | 23, 90 | jca 515 |
. 2
⊢ (𝜑 → (𝐶 ⊆ ∪ 𝐴 ∧ ∀𝑥 ∈ ∪ 𝐴
¬ 𝑥 ∈ (𝑁‘(∪ 𝐴
∖ {𝑥})))) |
92 | | sseq2 3903 |
. . . 4
⊢ (𝑧 = ∪
𝐴 → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ ∪ 𝐴)) |
93 | | difeq1 4006 |
. . . . . . . 8
⊢ (𝑧 = ∪
𝐴 → (𝑧 ∖ {𝑥}) = (∪ 𝐴 ∖ {𝑥})) |
94 | 93 | fveq2d 6678 |
. . . . . . 7
⊢ (𝑧 = ∪
𝐴 → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
95 | 94 | eleq2d 2818 |
. . . . . 6
⊢ (𝑧 = ∪
𝐴 → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
96 | 95 | notbid 321 |
. . . . 5
⊢ (𝑧 = ∪
𝐴 → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
97 | 96 | raleqbi1dv 3308 |
. . . 4
⊢ (𝑧 = ∪
𝐴 → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
98 | 92, 97 | anbi12d 634 |
. . 3
⊢ (𝑧 = ∪
𝐴 → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ ∪ 𝐴 ∧ ∀𝑥 ∈ ∪ 𝐴
¬ 𝑥 ∈ (𝑁‘(∪ 𝐴
∖ {𝑥}))))) |
99 | 98, 2 | elrab2 3591 |
. 2
⊢ (∪ 𝐴
∈ 𝑆 ↔ (∪ 𝐴
∈ 𝒫 𝑉 ∧
(𝐶 ⊆ ∪ 𝐴
∧ ∀𝑥 ∈
∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))))) |
100 | 10, 91, 99 | sylanbrc 586 |
1
⊢ (𝜑 → ∪ 𝐴
∈ 𝑆) |