Proof of Theorem neik0pk1imk0
Step | Hyp | Ref
| Expression |
1 | | neik0pk1imk0.k1 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥))) |
2 | | neik0pk1imk0.bex |
. . . . . . . 8
⊢ (𝜑 → 𝐵 ∈ 𝑉) |
3 | | pwidg 4121 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑉 → 𝐵 ∈ 𝒫 𝐵) |
4 | 2, 3 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐵) |
5 | | sseq2 3590 |
. . . . . . . . . 10
⊢ (𝑡 = 𝐵 → (𝑠 ⊆ 𝑡 ↔ 𝑠 ⊆ 𝐵)) |
6 | 5 | anbi2d 736 |
. . . . . . . . 9
⊢ (𝑡 = 𝐵 → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) ↔ (𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵))) |
7 | | eleq1 2676 |
. . . . . . . . 9
⊢ (𝑡 = 𝐵 → (𝑡 ∈ (𝑁‘𝑥) ↔ 𝐵 ∈ (𝑁‘𝑥))) |
8 | 6, 7 | imbi12d 333 |
. . . . . . . 8
⊢ (𝑡 = 𝐵 → (((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)) ↔ ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
9 | 8 | rspcv 3278 |
. . . . . . 7
⊢ (𝐵 ∈ 𝒫 𝐵 → (∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
10 | 4, 9 | syl 17 |
. . . . . 6
⊢ (𝜑 → (∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)) → ((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
11 | 10 | ralimdv 2946 |
. . . . 5
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)) → ∀𝑠 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
12 | 11 | ralimdv 2946 |
. . . 4
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵∀𝑡 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝑡) → 𝑡 ∈ (𝑁‘𝑥)) → ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
13 | 1, 12 | mpd 15 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥))) |
14 | | r19.23v 3005 |
. . . . . 6
⊢
(∀𝑠 ∈
𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)) ↔ (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥))) |
15 | 14 | biimpi 205 |
. . . . 5
⊢
(∀𝑠 ∈
𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)) → (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥))) |
16 | 15 | a1i 11 |
. . . 4
⊢ (𝜑 → (∀𝑠 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)) → (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
17 | 16 | ralimdv 2946 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 ∀𝑠 ∈ 𝒫 𝐵((𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)) → ∀𝑥 ∈ 𝐵 (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)))) |
18 | 13, 17 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥))) |
19 | | neik0pk1imk0.k0p |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅) |
20 | | neik0pk1imk0.n |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑁 ∈ (𝒫 𝒫 𝐵 ↑𝑚
𝐵)) |
21 | | elmapi 7765 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ (𝒫 𝒫
𝐵
↑𝑚 𝐵) → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
22 | 20, 21 | syl 17 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝑁:𝐵⟶𝒫 𝒫 𝐵) |
23 | 22 | ffvelrnda 6267 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁‘𝑥) ∈ 𝒫 𝒫 𝐵) |
24 | 23 | elpwid 4118 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑁‘𝑥) ⊆ 𝒫 𝐵) |
25 | 24 | sseld 3567 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑠 ∈ (𝑁‘𝑥) → 𝑠 ∈ 𝒫 𝐵)) |
26 | 25 | ancrd 575 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑠 ∈ (𝑁‘𝑥) → (𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ (𝑁‘𝑥)))) |
27 | 26 | eximdv 1833 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (∃𝑠 𝑠 ∈ (𝑁‘𝑥) → ∃𝑠(𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ (𝑁‘𝑥)))) |
28 | | n0 3890 |
. . . . . . . 8
⊢ ((𝑁‘𝑥) ≠ ∅ ↔ ∃𝑠 𝑠 ∈ (𝑁‘𝑥)) |
29 | | df-rex 2902 |
. . . . . . . 8
⊢
(∃𝑠 ∈
𝒫 𝐵𝑠 ∈ (𝑁‘𝑥) ↔ ∃𝑠(𝑠 ∈ 𝒫 𝐵 ∧ 𝑠 ∈ (𝑁‘𝑥))) |
30 | 27, 28, 29 | 3imtr4g 284 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑁‘𝑥) ≠ ∅ → ∃𝑠 ∈ 𝒫 𝐵𝑠 ∈ (𝑁‘𝑥))) |
31 | 30 | imp 444 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑁‘𝑥) ≠ ∅) → ∃𝑠 ∈ 𝒫 𝐵𝑠 ∈ (𝑁‘𝑥)) |
32 | | elpwi 4117 |
. . . . . . . . . 10
⊢ (𝑠 ∈ 𝒫 𝐵 → 𝑠 ⊆ 𝐵) |
33 | 25, 32 | syl6 34 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → (𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵)) |
34 | 33 | alrimiv 1842 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑠(𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵)) |
35 | | alral 2912 |
. . . . . . . 8
⊢
(∀𝑠(𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵) → ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵)) |
36 | 34, 35 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵)) |
37 | 36 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑁‘𝑥) ≠ ∅) → ∀𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) → 𝑠 ⊆ 𝐵)) |
38 | 31, 37 | r19.29imd 3056 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ 𝐵) ∧ (𝑁‘𝑥) ≠ ∅) → ∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵)) |
39 | 38 | ex 449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐵) → ((𝑁‘𝑥) ≠ ∅ → ∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵))) |
40 | 39 | ralimdva 2945 |
. . 3
⊢ (𝜑 → (∀𝑥 ∈ 𝐵 (𝑁‘𝑥) ≠ ∅ → ∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵))) |
41 | 19, 40 | mpd 15 |
. 2
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵)) |
42 | | ralim 2932 |
. 2
⊢
(∀𝑥 ∈
𝐵 (∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → 𝐵 ∈ (𝑁‘𝑥)) → (∀𝑥 ∈ 𝐵 ∃𝑠 ∈ 𝒫 𝐵(𝑠 ∈ (𝑁‘𝑥) ∧ 𝑠 ⊆ 𝐵) → ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥))) |
43 | 18, 41, 42 | sylc 63 |
1
⊢ (𝜑 → ∀𝑥 ∈ 𝐵 𝐵 ∈ (𝑁‘𝑥)) |