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 ( ( 𝐴𝑉 ∧ ∀ 𝑥𝐴 𝐵 ∈ ( 𝑓𝑥 ) ) → ∃ 𝑔𝑥𝐴 ( 𝑔𝑥 ) ∈ ( 𝑓𝑥 ) )