Metamath Proof Explorer

Theorem ac5num

Description: A version of ac5b with the choice as a hypothesis. (Contributed by Mario Carneiro, 27-Aug-2015)

Ref Expression
Assertion ac5num ⊢⋃A∈dom⁡card∧¬∅∈A→∃ff:A⟶⋃A∧∀x∈Af⁡x∈x

Proof

Step Hyp Ref Expression
1 uniexr ⊢⋃A∈dom⁡card→A∈V
2 dfac8b ⊢⋃A∈dom⁡card→∃rrWe⋃A
3 dfac8c ⊢A∈V→∃rrWe⋃A→∃g∀x∈Ax≠∅→g⁡x∈x
4 1 2 3 sylc ⊢⋃A∈dom⁡card→∃g∀x∈Ax≠∅→g⁡x∈x
5 4 adantr ⊢⋃A∈dom⁡card∧¬∅∈A→∃g∀x∈Ax≠∅→g⁡x∈x
6 1 ad2antrr ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→A∈V
7 6 mptexd ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→y∈A⟼g⁡y∈V
8 nelne2 ⊢x∈A∧¬∅∈A→x≠∅
9 8 ancoms ⊢¬∅∈A∧x∈A→x≠∅
10 9 adantll ⊢⋃A∈dom⁡card∧¬∅∈A∧x∈A→x≠∅
11 pm2.27 ⊢x≠∅→x≠∅→g⁡x∈x→g⁡x∈x
12 10 11 syl ⊢⋃A∈dom⁡card∧¬∅∈A∧x∈A→x≠∅→g⁡x∈x→g⁡x∈x
13 12 ralimdva ⊢⋃A∈dom⁡card∧¬∅∈A→∀x∈Ax≠∅→g⁡x∈x→∀x∈Ag⁡x∈x
14 13 imp ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→∀x∈Ag⁡x∈x
15 fveq2 ⊢x=y→g⁡x=g⁡y
16 id ⊢x=y→x=y
17 15 16 eleq12d ⊢x=y→g⁡x∈x↔g⁡y∈y
18 17 rspccva ⊢∀x∈Ag⁡x∈x∧y∈A→g⁡y∈y
19 14 18 sylan ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x∧y∈A→g⁡y∈y
20 elunii ⊢g⁡y∈y∧y∈A→g⁡y∈⋃A
21 19 20 sylancom ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x∧y∈A→g⁡y∈⋃A
22 21 fmpttd ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→y∈A⟼g⁡y:A⟶⋃A
23 fveq2 ⊢y=x→g⁡y=g⁡x
24 eqid ⊢y∈A⟼g⁡y=y∈A⟼g⁡y
25 fvex ⊢g⁡x∈V
26 23 24 25 fvmpt ⊢x∈A→y∈A⟼g⁡y⁡x=g⁡x
27 26 eleq1d ⊢x∈A→y∈A⟼g⁡y⁡x∈x↔g⁡x∈x
28 27 ralbiia ⊢∀x∈Ay∈A⟼g⁡y⁡x∈x↔∀x∈Ag⁡x∈x
29 14 28 sylibr ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→∀x∈Ay∈A⟼g⁡y⁡x∈x
30 22 29 jca ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→y∈A⟼g⁡y:A⟶⋃A∧∀x∈Ay∈A⟼g⁡y⁡x∈x
31 feq1 ⊢f=y∈A⟼g⁡y→f:A⟶⋃A↔y∈A⟼g⁡y:A⟶⋃A
32 fveq1 ⊢f=y∈A⟼g⁡y→f⁡x=y∈A⟼g⁡y⁡x
33 32 eleq1d ⊢f=y∈A⟼g⁡y→f⁡x∈x↔y∈A⟼g⁡y⁡x∈x
34 33 ralbidv ⊢f=y∈A⟼g⁡y→∀x∈Af⁡x∈x↔∀x∈Ay∈A⟼g⁡y⁡x∈x
35 31 34 anbi12d ⊢f=y∈A⟼g⁡y→f:A⟶⋃A∧∀x∈Af⁡x∈x↔y∈A⟼g⁡y:A⟶⋃A∧∀x∈Ay∈A⟼g⁡y⁡x∈x
36 7 30 35 spcedv ⊢⋃A∈dom⁡card∧¬∅∈A∧∀x∈Ax≠∅→g⁡x∈x→∃ff:A⟶⋃A∧∀x∈Af⁡x∈x
37 5 36 exlimddv ⊢⋃A∈dom⁡card∧¬∅∈A→∃ff:A⟶⋃A∧∀x∈Af⁡x∈x