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 ⊢A∈V∧∀x∈AB∈f⁡x→∃g∀x∈Ag⁡x∈f⁡x

Proof

Step Hyp Ref Expression
1 fvssunirn ⊢f⁡x⊆⋃ran⁡f
2 simpr ⊢x∈A∧B∈f⁡x→B∈f⁡x
3 1 2 sselid ⊢x∈A∧B∈f⁡x→B∈⋃ran⁡f
4 3 ralimiaa ⊢∀x∈AB∈f⁡x→∀x∈AB∈⋃ran⁡f
5 eqid ⊢x∈A⟼B=x∈A⟼B
6 5 fmpt ⊢∀x∈AB∈⋃ran⁡f↔x∈A⟼B:A⟶⋃ran⁡f
7 4 6 sylib ⊢∀x∈AB∈f⁡x→x∈A⟼B:A⟶⋃ran⁡f
8 id ⊢A∈V→A∈V
9 vex ⊢f∈V
10 9 rnex ⊢ran⁡f∈V
11 10 uniex ⊢⋃ran⁡f∈V
12 fex2 ⊢x∈A⟼B:A⟶⋃ran⁡f∧A∈V∧⋃ran⁡f∈V→x∈A⟼B∈V
13 11 12 mp3an3 ⊢x∈A⟼B:A⟶⋃ran⁡f∧A∈V→x∈A⟼B∈V
14 7 8 13 syl2anr ⊢A∈V∧∀x∈AB∈f⁡x→x∈A⟼B∈V
15 5 fvmpt2 ⊢x∈A∧B∈f⁡x→x∈A⟼B⁡x=B
16 15 2 eqeltrd ⊢x∈A∧B∈f⁡x→x∈A⟼B⁡x∈f⁡x
17 16 ralimiaa ⊢∀x∈AB∈f⁡x→∀x∈Ax∈A⟼B⁡x∈f⁡x
18 17 adantl ⊢A∈V∧∀x∈AB∈f⁡x→∀x∈Ax∈A⟼B⁡x∈f⁡x
19 nfmpt1 ⊢Ⅎ_xx∈A⟼B
20 19 nfeq2 ⊢Ⅎxg=x∈A⟼B
21 fveq1 ⊢g=x∈A⟼B→g⁡x=x∈A⟼B⁡x
22 21 eleq1d ⊢g=x∈A⟼B→g⁡x∈f⁡x↔x∈A⟼B⁡x∈f⁡x
23 20 22 ralbid ⊢g=x∈A⟼B→∀x∈Ag⁡x∈f⁡x↔∀x∈Ax∈A⟼B⁡x∈f⁡x
24 14 18 23 spcedv ⊢A∈V∧∀x∈AB∈f⁡x→∃g∀x∈Ag⁡x∈f⁡x