Step | Hyp | Ref
| Expression |
1 | | lbsext.a |
. . . . 5
⊢ (𝜑 → 𝐴 ⊆ 𝑆) |
2 | | lbsext.s |
. . . . . 6
⊢ 𝑆 = {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} |
3 | | ssrab2 3650 |
. . . . . 6
⊢ {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⊆ 𝒫 𝑉 |
4 | 2, 3 | eqsstri 3598 |
. . . . 5
⊢ 𝑆 ⊆ 𝒫 𝑉 |
5 | 1, 4 | syl6ss 3580 |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ 𝒫 𝑉) |
6 | | sspwuni 4547 |
. . . 4
⊢ (𝐴 ⊆ 𝒫 𝑉 ↔ ∪ 𝐴
⊆ 𝑉) |
7 | 5, 6 | sylib 207 |
. . 3
⊢ (𝜑 → ∪ 𝐴
⊆ 𝑉) |
8 | | lbsext.v |
. . . . 5
⊢ 𝑉 = (Base‘𝑊) |
9 | | fvex 6113 |
. . . . 5
⊢
(Base‘𝑊)
∈ V |
10 | 8, 9 | eqeltri 2684 |
. . . 4
⊢ 𝑉 ∈ V |
11 | 10 | elpw2 4755 |
. . 3
⊢ (∪ 𝐴
∈ 𝒫 𝑉 ↔
∪ 𝐴 ⊆ 𝑉) |
12 | 7, 11 | sylibr 223 |
. 2
⊢ (𝜑 → ∪ 𝐴
∈ 𝒫 𝑉) |
13 | | ssintub 4430 |
. . . . 5
⊢ 𝐶 ⊆ ∩ {𝑧
∈ 𝒫 𝑉 ∣
𝐶 ⊆ 𝑧} |
14 | | simpl 472 |
. . . . . . . . . 10
⊢ ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶 ⊆ 𝑧) |
15 | 14 | a1i 11 |
. . . . . . . . 9
⊢ (𝑧 ∈ 𝒫 𝑉 → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) → 𝐶 ⊆ 𝑧)) |
16 | 15 | ss2rabi 3647 |
. . . . . . . 8
⊢ {𝑧 ∈ 𝒫 𝑉 ∣ (𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})))} ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} |
17 | 2, 16 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑆 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} |
18 | 1, 17 | syl6ss 3580 |
. . . . . 6
⊢ (𝜑 → 𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧}) |
19 | | intss 4433 |
. . . . . 6
⊢ (𝐴 ⊆ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} → ∩ {𝑧 ∈ 𝒫 𝑉 ∣ 𝐶 ⊆ 𝑧} ⊆ ∩ 𝐴) |
20 | 18, 19 | syl 17 |
. . . . 5
⊢ (𝜑 → ∩ {𝑧
∈ 𝒫 𝑉 ∣
𝐶 ⊆ 𝑧} ⊆ ∩ 𝐴) |
21 | 13, 20 | syl5ss 3579 |
. . . 4
⊢ (𝜑 → 𝐶 ⊆ ∩ 𝐴) |
22 | | lbsext.z |
. . . . 5
⊢ (𝜑 → 𝐴 ≠ ∅) |
23 | | intssuni 4434 |
. . . . 5
⊢ (𝐴 ≠ ∅ → ∩ 𝐴
⊆ ∪ 𝐴) |
24 | 22, 23 | syl 17 |
. . . 4
⊢ (𝜑 → ∩ 𝐴
⊆ ∪ 𝐴) |
25 | 21, 24 | sstrd 3578 |
. . 3
⊢ (𝜑 → 𝐶 ⊆ ∪ 𝐴) |
26 | | eluni2 4376 |
. . . . 5
⊢ (𝑥 ∈ ∪ 𝐴
↔ ∃𝑦 ∈
𝐴 𝑥 ∈ 𝑦) |
27 | | simpll1 1093 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝜑) |
28 | | lbsext.w |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑊 ∈ LVec) |
29 | | lveclmod 18927 |
. . . . . . . . . . . . 13
⊢ (𝑊 ∈ LVec → 𝑊 ∈ LMod) |
30 | 28, 29 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑊 ∈ LMod) |
31 | 27, 30 | syl 17 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑊 ∈ LMod) |
32 | 27, 1 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝐴 ⊆ 𝑆) |
33 | | lbsext.r |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → [⊊] Or 𝐴) |
34 | 27, 33 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → [⊊] Or 𝐴) |
35 | | simpll2 1094 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑦 ∈ 𝐴) |
36 | | simplr 788 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑢 ∈ 𝐴) |
37 | | sorpssun 6842 |
. . . . . . . . . . . . . . . 16
⊢ ((
[⊊] Or 𝐴
∧ (𝑦 ∈ 𝐴 ∧ 𝑢 ∈ 𝐴)) → (𝑦 ∪ 𝑢) ∈ 𝐴) |
38 | 34, 35, 36, 37 | syl12anc 1316 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝐴) |
39 | 32, 38 | sseldd 3569 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝑆) |
40 | 4, 39 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ∈ 𝒫 𝑉) |
41 | 40 | elpwid 4118 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑦 ∪ 𝑢) ⊆ 𝑉) |
42 | 41 | ssdifssd 3710 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ((𝑦 ∪ 𝑢) ∖ {𝑥}) ⊆ 𝑉) |
43 | | ssun2 3739 |
. . . . . . . . . . . 12
⊢ 𝑢 ⊆ (𝑦 ∪ 𝑢) |
44 | | ssdif 3707 |
. . . . . . . . . . . 12
⊢ (𝑢 ⊆ (𝑦 ∪ 𝑢) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
45 | 43, 44 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
46 | | lbsext.n |
. . . . . . . . . . . 12
⊢ 𝑁 = (LSpan‘𝑊) |
47 | 8, 46 | lspss 18805 |
. . . . . . . . . . 11
⊢ ((𝑊 ∈ LMod ∧ ((𝑦 ∪ 𝑢) ∖ {𝑥}) ⊆ 𝑉 ∧ (𝑢 ∖ {𝑥}) ⊆ ((𝑦 ∪ 𝑢) ∖ {𝑥})) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
48 | 31, 42, 45, 47 | syl3anc 1318 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → (𝑁‘(𝑢 ∖ {𝑥})) ⊆ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
49 | | simpr 476 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
50 | 48, 49 | sseldd 3569 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
51 | | sseq2 3590 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ (𝑦 ∪ 𝑢))) |
52 | | difeq1 3683 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑧 ∖ {𝑥}) = ((𝑦 ∪ 𝑢) ∖ {𝑥})) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
54 | 53 | eleq2d 2673 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
55 | 54 | notbid 307 |
. . . . . . . . . . . . . . . 16
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
56 | 55 | raleqbi1dv 3123 |
. . . . . . . . . . . . . . 15
⊢ (𝑧 = (𝑦 ∪ 𝑢) → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
57 | 51, 56 | anbi12d 743 |
. . . . . . . . . . . . . 14
⊢ (𝑧 = (𝑦 ∪ 𝑢) → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))))) |
58 | 57, 2 | elrab2 3333 |
. . . . . . . . . . . . 13
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 ↔ ((𝑦 ∪ 𝑢) ∈ 𝒫 𝑉 ∧ (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))))) |
59 | 58 | simprbi 479 |
. . . . . . . . . . . 12
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 → (𝐶 ⊆ (𝑦 ∪ 𝑢) ∧ ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
60 | 59 | simprd 478 |
. . . . . . . . . . 11
⊢ ((𝑦 ∪ 𝑢) ∈ 𝑆 → ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
61 | 39, 60 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ∀𝑥 ∈ (𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
62 | | simpll3 1095 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ 𝑦) |
63 | | elun1 3742 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑦 → 𝑥 ∈ (𝑦 ∪ 𝑢)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → 𝑥 ∈ (𝑦 ∪ 𝑢)) |
65 | | rsp 2913 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
(𝑦 ∪ 𝑢) ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})) → (𝑥 ∈ (𝑦 ∪ 𝑢) → ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥})))) |
66 | 61, 64, 65 | sylc 63 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) ∧ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) → ¬ 𝑥 ∈ (𝑁‘((𝑦 ∪ 𝑢) ∖ {𝑥}))) |
67 | 50, 66 | pm2.65da 598 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) ∧ 𝑢 ∈ 𝐴) → ¬ 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
68 | 67 | nrexdv 2984 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → ¬ ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
69 | | lbsext.j |
. . . . . . . . . . . . . . . 16
⊢ 𝐽 = (LBasis‘𝑊) |
70 | | lbsext.c |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐶 ⊆ 𝑉) |
71 | | lbsext.x |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → ∀𝑥 ∈ 𝐶 ¬ 𝑥 ∈ (𝑁‘(𝐶 ∖ {𝑥}))) |
72 | | lbsext.p |
. . . . . . . . . . . . . . . 16
⊢ 𝑃 = (LSubSp‘𝑊) |
73 | | lbsext.t |
. . . . . . . . . . . . . . . 16
⊢ 𝑇 = ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) |
74 | 8, 69, 46, 28, 70, 71, 2, 72, 1, 22, 33, 73 | lbsextlem2 18980 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → (𝑇 ∈ 𝑃 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇)) |
75 | 74 | simpld 474 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ∈ 𝑃) |
76 | 8, 72 | lssss 18758 |
. . . . . . . . . . . . . 14
⊢ (𝑇 ∈ 𝑃 → 𝑇 ⊆ 𝑉) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑇 ⊆ 𝑉) |
78 | 74 | simprd 478 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (∪ 𝐴
∖ {𝑥}) ⊆ 𝑇) |
79 | 8, 46 | lspss 18805 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ⊆ 𝑉 ∧ (∪ 𝐴 ∖ {𝑥}) ⊆ 𝑇) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ (𝑁‘𝑇)) |
80 | 30, 77, 78, 79 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ (𝑁‘𝑇)) |
81 | 72, 46 | lspid 18803 |
. . . . . . . . . . . . 13
⊢ ((𝑊 ∈ LMod ∧ 𝑇 ∈ 𝑃) → (𝑁‘𝑇) = 𝑇) |
82 | 30, 75, 81 | syl2anc 691 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑁‘𝑇) = 𝑇) |
83 | 80, 82 | sseqtrd 3604 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ 𝑇) |
84 | 83 | 3ad2ant1 1075 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ 𝑇) |
85 | 84, 73 | syl6sseq 3614 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑁‘(∪ 𝐴 ∖ {𝑥})) ⊆ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥}))) |
86 | 85 | sseld 3567 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})) → 𝑥 ∈ ∪
𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})))) |
87 | | eliun 4460 |
. . . . . . . 8
⊢ (𝑥 ∈ ∪ 𝑢 ∈ 𝐴 (𝑁‘(𝑢 ∖ {𝑥})) ↔ ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥}))) |
88 | 86, 87 | syl6ib 240 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → (𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})) → ∃𝑢 ∈ 𝐴 𝑥 ∈ (𝑁‘(𝑢 ∖ {𝑥})))) |
89 | 68, 88 | mtod 188 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑦 ∈ 𝐴 ∧ 𝑥 ∈ 𝑦) → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
90 | 89 | rexlimdv3a 3015 |
. . . . 5
⊢ (𝜑 → (∃𝑦 ∈ 𝐴 𝑥 ∈ 𝑦 → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
91 | 26, 90 | syl5bi 231 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ∪ 𝐴 → ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
92 | 91 | ralrimiv 2948 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
93 | 25, 92 | jca 553 |
. 2
⊢ (𝜑 → (𝐶 ⊆ ∪ 𝐴 ∧ ∀𝑥 ∈ ∪ 𝐴
¬ 𝑥 ∈ (𝑁‘(∪ 𝐴
∖ {𝑥})))) |
94 | | sseq2 3590 |
. . . 4
⊢ (𝑧 = ∪
𝐴 → (𝐶 ⊆ 𝑧 ↔ 𝐶 ⊆ ∪ 𝐴)) |
95 | | difeq1 3683 |
. . . . . . . 8
⊢ (𝑧 = ∪
𝐴 → (𝑧 ∖ {𝑥}) = (∪ 𝐴 ∖ {𝑥})) |
96 | 95 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑧 = ∪
𝐴 → (𝑁‘(𝑧 ∖ {𝑥})) = (𝑁‘(∪ 𝐴 ∖ {𝑥}))) |
97 | 96 | eleq2d 2673 |
. . . . . 6
⊢ (𝑧 = ∪
𝐴 → (𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
98 | 97 | notbid 307 |
. . . . 5
⊢ (𝑧 = ∪
𝐴 → (¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
99 | 98 | raleqbi1dv 3123 |
. . . 4
⊢ (𝑧 = ∪
𝐴 → (∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥})) ↔ ∀𝑥 ∈ ∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥})))) |
100 | 94, 99 | anbi12d 743 |
. . 3
⊢ (𝑧 = ∪
𝐴 → ((𝐶 ⊆ 𝑧 ∧ ∀𝑥 ∈ 𝑧 ¬ 𝑥 ∈ (𝑁‘(𝑧 ∖ {𝑥}))) ↔ (𝐶 ⊆ ∪ 𝐴 ∧ ∀𝑥 ∈ ∪ 𝐴
¬ 𝑥 ∈ (𝑁‘(∪ 𝐴
∖ {𝑥}))))) |
101 | 100, 2 | elrab2 3333 |
. 2
⊢ (∪ 𝐴
∈ 𝑆 ↔ (∪ 𝐴
∈ 𝒫 𝑉 ∧
(𝐶 ⊆ ∪ 𝐴
∧ ∀𝑥 ∈
∪ 𝐴 ¬ 𝑥 ∈ (𝑁‘(∪ 𝐴 ∖ {𝑥}))))) |
102 | 12, 93, 101 | sylanbrc 695 |
1
⊢ (𝜑 → ∪ 𝐴
∈ 𝑆) |