Proof of Theorem acnlem
| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | fvssunirn 6939 | . . . . . 6
⊢ (𝑓‘𝑥) ⊆ ∪ ran
𝑓 | 
| 2 |  | simpr 484 | . . . . . 6
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝑓‘𝑥)) → 𝐵 ∈ (𝑓‘𝑥)) | 
| 3 | 1, 2 | sselid 3981 | . . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝑓‘𝑥)) → 𝐵 ∈ ∪ ran
𝑓) | 
| 4 | 3 | ralimiaa 3082 | . . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑓‘𝑥) → ∀𝑥 ∈ 𝐴 𝐵 ∈ ∪ ran
𝑓) | 
| 5 |  | eqid 2737 | . . . . 5
⊢ (𝑥 ∈ 𝐴 ↦ 𝐵) = (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 6 | 5 | fmpt 7130 | . . . 4
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ ∪ ran
𝑓 ↔ (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶∪ ran
𝑓) | 
| 7 | 4, 6 | sylib 218 | . . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑓‘𝑥) → (𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶∪ ran
𝑓) | 
| 8 |  | id 22 | . . 3
⊢ (𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉) | 
| 9 |  | vex 3484 | . . . . . 6
⊢ 𝑓 ∈ V | 
| 10 | 9 | rnex 7932 | . . . . 5
⊢ ran 𝑓 ∈ V | 
| 11 | 10 | uniex 7761 | . . . 4
⊢ ∪ ran 𝑓 ∈ V | 
| 12 |  | fex2 7958 | . . . 4
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶∪ ran
𝑓 ∧ 𝐴 ∈ 𝑉 ∧ ∪ ran
𝑓 ∈ V) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | 
| 13 | 11, 12 | mp3an3 1452 | . . 3
⊢ (((𝑥 ∈ 𝐴 ↦ 𝐵):𝐴⟶∪ ran
𝑓 ∧ 𝐴 ∈ 𝑉) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | 
| 14 | 7, 8, 13 | syl2anr 597 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → (𝑥 ∈ 𝐴 ↦ 𝐵) ∈ V) | 
| 15 | 5 | fvmpt2 7027 | . . . . 5
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) = 𝐵) | 
| 16 | 15, 2 | eqeltrd 2841 | . . . 4
⊢ ((𝑥 ∈ 𝐴 ∧ 𝐵 ∈ (𝑓‘𝑥)) → ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑓‘𝑥)) | 
| 17 | 16 | ralimiaa 3082 | . . 3
⊢
(∀𝑥 ∈
𝐴 𝐵 ∈ (𝑓‘𝑥) → ∀𝑥 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑓‘𝑥)) | 
| 18 | 17 | adantl 481 | . 2
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∀𝑥 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑓‘𝑥)) | 
| 19 |  | nfmpt1 5250 | . . . 4
⊢
Ⅎ𝑥(𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 20 | 19 | nfeq2 2923 | . . 3
⊢
Ⅎ𝑥 𝑔 = (𝑥 ∈ 𝐴 ↦ 𝐵) | 
| 21 |  | fveq1 6905 | . . . 4
⊢ (𝑔 = (𝑥 ∈ 𝐴 ↦ 𝐵) → (𝑔‘𝑥) = ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥)) | 
| 22 | 21 | eleq1d 2826 | . . 3
⊢ (𝑔 = (𝑥 ∈ 𝐴 ↦ 𝐵) → ((𝑔‘𝑥) ∈ (𝑓‘𝑥) ↔ ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑓‘𝑥))) | 
| 23 | 20, 22 | ralbid 3273 | . 2
⊢ (𝑔 = (𝑥 ∈ 𝐴 ↦ 𝐵) → (∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥) ↔ ∀𝑥 ∈ 𝐴 ((𝑥 ∈ 𝐴 ↦ 𝐵)‘𝑥) ∈ (𝑓‘𝑥))) | 
| 24 | 14, 18, 23 | spcedv 3598 | 1
⊢ ((𝐴 ∈ 𝑉 ∧ ∀𝑥 ∈ 𝐴 𝐵 ∈ (𝑓‘𝑥)) → ∃𝑔∀𝑥 ∈ 𝐴 (𝑔‘𝑥) ∈ (𝑓‘𝑥)) |