Step | Hyp | Ref
| Expression |
1 | | acsmapd.4 |
. . . 4
⊢ (𝜑 → 𝑇 ⊆ (𝑁‘𝑆)) |
2 | | fvex 6113 |
. . . . 5
⊢ (𝑁‘𝑆) ∈ V |
3 | 2 | ssex 4730 |
. . . 4
⊢ (𝑇 ⊆ (𝑁‘𝑆) → 𝑇 ∈ V) |
4 | 1, 3 | syl 17 |
. . 3
⊢ (𝜑 → 𝑇 ∈ V) |
5 | 1 | sseld 3567 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ 𝑇 → 𝑥 ∈ (𝑁‘𝑆))) |
6 | | acsmapd.1 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ (ACS‘𝑋)) |
7 | | acsmapd.2 |
. . . . . 6
⊢ 𝑁 = (mrCls‘𝐴) |
8 | | acsmapd.3 |
. . . . . 6
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
9 | 6, 7, 8 | acsficl2d 16999 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (𝑁‘𝑆) ↔ ∃𝑦 ∈ (𝒫 𝑆 ∩ Fin)𝑥 ∈ (𝑁‘𝑦))) |
10 | 5, 9 | sylibd 228 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ 𝑇 → ∃𝑦 ∈ (𝒫 𝑆 ∩ Fin)𝑥 ∈ (𝑁‘𝑦))) |
11 | 10 | ralrimiv 2948 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝑇 ∃𝑦 ∈ (𝒫 𝑆 ∩ Fin)𝑥 ∈ (𝑁‘𝑦)) |
12 | | fveq2 6103 |
. . . . 5
⊢ (𝑦 = (𝑓‘𝑥) → (𝑁‘𝑦) = (𝑁‘(𝑓‘𝑥))) |
13 | 12 | eleq2d 2673 |
. . . 4
⊢ (𝑦 = (𝑓‘𝑥) → (𝑥 ∈ (𝑁‘𝑦) ↔ 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) |
14 | 13 | ac6sg 9193 |
. . 3
⊢ (𝑇 ∈ V → (∀𝑥 ∈ 𝑇 ∃𝑦 ∈ (𝒫 𝑆 ∩ Fin)𝑥 ∈ (𝑁‘𝑦) → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥))))) |
15 | 4, 11, 14 | sylc 63 |
. 2
⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) |
16 | | simprl 790 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → 𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin)) |
17 | | nfv 1830 |
. . . . . . . 8
⊢
Ⅎ𝑥𝜑 |
18 | | nfv 1830 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) |
19 | | nfra1 2925 |
. . . . . . . . 9
⊢
Ⅎ𝑥∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)) |
20 | 18, 19 | nfan 1816 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥))) |
21 | 17, 20 | nfan 1816 |
. . . . . . 7
⊢
Ⅎ𝑥(𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) |
22 | 6 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝐴 ∈ (ACS‘𝑋)) |
23 | 22 | acsmred 16140 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝐴 ∈ (Moore‘𝑋)) |
24 | | simplrl 796 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin)) |
25 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) → 𝑓 Fn 𝑇) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑓 Fn 𝑇) |
27 | | fnfvelrn 6264 |
. . . . . . . . . . . . 13
⊢ ((𝑓 Fn 𝑇 ∧ 𝑥 ∈ 𝑇) → (𝑓‘𝑥) ∈ ran 𝑓) |
28 | 26, 27 | sylancom 698 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → (𝑓‘𝑥) ∈ ran 𝑓) |
29 | 28 | snssd 4281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → {(𝑓‘𝑥)} ⊆ ran 𝑓) |
30 | 29 | unissd 4398 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → ∪
{(𝑓‘𝑥)} ⊆ ∪ ran 𝑓) |
31 | | frn 5966 |
. . . . . . . . . . . . . 14
⊢ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) → ran 𝑓 ⊆ (𝒫 𝑆 ∩ Fin)) |
32 | 31 | unissd 4398 |
. . . . . . . . . . . . 13
⊢ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) → ∪ ran 𝑓 ⊆ ∪
(𝒫 𝑆 ∩
Fin)) |
33 | | unifpw 8152 |
. . . . . . . . . . . . 13
⊢ ∪ (𝒫 𝑆 ∩ Fin) = 𝑆 |
34 | 32, 33 | syl6sseq 3614 |
. . . . . . . . . . . 12
⊢ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) → ∪ ran 𝑓 ⊆ 𝑆) |
35 | 24, 34 | syl 17 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → ∪ ran
𝑓 ⊆ 𝑆) |
36 | 8 | ad2antrr 758 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑆 ⊆ 𝑋) |
37 | 35, 36 | sstrd 3578 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → ∪ ran
𝑓 ⊆ 𝑋) |
38 | 23, 7, 30, 37 | mrcssd 16107 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → (𝑁‘∪ {(𝑓‘𝑥)}) ⊆ (𝑁‘∪ ran
𝑓)) |
39 | | simprr 792 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥))) |
40 | 39 | r19.21bi 2916 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ (𝑁‘(𝑓‘𝑥))) |
41 | | fvex 6113 |
. . . . . . . . . . . 12
⊢ (𝑓‘𝑥) ∈ V |
42 | 41 | unisn 4387 |
. . . . . . . . . . 11
⊢ ∪ {(𝑓‘𝑥)} = (𝑓‘𝑥) |
43 | 42 | fveq2i 6106 |
. . . . . . . . . 10
⊢ (𝑁‘∪ {(𝑓‘𝑥)}) = (𝑁‘(𝑓‘𝑥)) |
44 | 40, 43 | syl6eleqr 2699 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ (𝑁‘∪ {(𝑓‘𝑥)})) |
45 | 38, 44 | sseldd 3569 |
. . . . . . . 8
⊢ (((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) ∧ 𝑥 ∈ 𝑇) → 𝑥 ∈ (𝑁‘∪ ran
𝑓)) |
46 | 45 | ex 449 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → (𝑥 ∈ 𝑇 → 𝑥 ∈ (𝑁‘∪ ran
𝑓))) |
47 | 21, 46 | alrimi 2069 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → ∀𝑥(𝑥 ∈ 𝑇 → 𝑥 ∈ (𝑁‘∪ ran
𝑓))) |
48 | | dfss2 3557 |
. . . . . 6
⊢ (𝑇 ⊆ (𝑁‘∪ ran
𝑓) ↔ ∀𝑥(𝑥 ∈ 𝑇 → 𝑥 ∈ (𝑁‘∪ ran
𝑓))) |
49 | 47, 48 | sylibr 223 |
. . . . 5
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → 𝑇 ⊆ (𝑁‘∪ ran
𝑓)) |
50 | 16, 49 | jca 553 |
. . . 4
⊢ ((𝜑 ∧ (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥)))) → (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran
𝑓))) |
51 | 50 | ex 449 |
. . 3
⊢ (𝜑 → ((𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥))) → (𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran
𝑓)))) |
52 | 51 | eximdv 1833 |
. 2
⊢ (𝜑 → (∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ ∀𝑥 ∈ 𝑇 𝑥 ∈ (𝑁‘(𝑓‘𝑥))) → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran
𝑓)))) |
53 | 15, 52 | mpd 15 |
1
⊢ (𝜑 → ∃𝑓(𝑓:𝑇⟶(𝒫 𝑆 ∩ Fin) ∧ 𝑇 ⊆ (𝑁‘∪ ran
𝑓))) |