Metamath Proof Explorer

Theorem acnlem

Description: Construct a mapping satisfying the consequent of isacn . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acnlem ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢ ( 𝑓 ‘ 𝑥 ) ⊆ ∪ ran 𝑓
2 simpr ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) )
3 1 2 sselid ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → 𝐵 ∈ ∪ ran 𝑓 )
4 3 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ∪ ran 𝑓 )
5 eqid ⊢ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
6 5 fmpt ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ∪ ran 𝑓 ↔ ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ∪ ran 𝑓 )
7 4 6 sylib ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ∪ ran 𝑓 )
8 id ⊢ ( 𝐴 ∈ 𝑉 → 𝐴 ∈ 𝑉 )
9 vex ⊢ 𝑓 ∈ V
10 9 rnex ⊢ ran 𝑓 ∈ V
11 10 uniex ⊢ ∪ ran 𝑓 ∈ V
12 fex2 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ∪ ran 𝑓 ∧ 𝐴 ∈ 𝑉 ∧ ∪ ran 𝑓 ∈ V ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
13 11 12 mp3an3 ⊢ ( ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) : 𝐴 ⟶ ∪ ran 𝑓 ∧ 𝐴 ∈ 𝑉 ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
14 7 8 13 syl2anr ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ V )
15 5 fvmpt2 ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) = 𝐵 )
16 15 2 eqeltrd ⊢ ( ( 𝑥 ∈ 𝐴 ∧ 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
17 16 ralimiaa ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
18 17 adantl ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )
19 nfmpt1 ⊢ Ⅎ 𝑥 ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
20 19 nfeq2 ⊢ Ⅎ 𝑥 𝑔 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 )
21 fveq1 ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( 𝑔 ‘ 𝑥 ) = ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) )
22 21 eleq1d ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ↔ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
23 20 22 ralbid ⊢ ( 𝑔 = ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) → ( ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ↔ ∀ 𝑥 ∈ 𝐴 ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) ) )
24 14 18 23 spcedv ⊢ ( ( 𝐴 ∈ 𝑉 ∧ ∀ 𝑥 ∈ 𝐴 𝐵 ∈ ( 𝑓 ‘ 𝑥 ) ) → ∃ 𝑔 ∀ 𝑥 ∈ 𝐴 ( 𝑔 ‘ 𝑥 ) ∈ ( 𝑓 ‘ 𝑥 ) )