Metamath Proof Explorer

Theorem ac6c4

Description: Equivalent of Axiom of Choice. B is a collection B ( x ) of nonempty sets. (Contributed by Mario Carneiro, 22-Mar-2013)

Ref Expression
Hypotheses ac6c4.1 ⊢A∈V
ac6c4.2 ⊢B∈V
Assertion ac6c4 ⊢∀x∈AB≠∅→∃ffFnA∧∀x∈Af⁡x∈B

Proof

Step Hyp Ref Expression
1 ac6c4.1 ⊢A∈V
2 ac6c4.2 ⊢B∈V
3 nfv ⊢ℲzB≠∅
4 nfcsb1v ⊢Ⅎ_x⦋z/x⦌B
5 nfcv ⊢Ⅎ_x∅
6 4 5 nfne ⊢Ⅎx⦋z/x⦌B≠∅
7 csbeq1a ⊢x=z→B=⦋z/x⦌B
8 7 neeq1d ⊢x=z→B≠∅↔⦋z/x⦌B≠∅
9 3 6 8 cbvralw ⊢∀x∈AB≠∅↔∀z∈A⦋z/x⦌B≠∅
10 n0 ⊢⦋z/x⦌B≠∅↔∃yy∈⦋z/x⦌B
11 nfv ⊢Ⅎyz∈A
12 nfre1 ⊢Ⅎy∃y∈⋃x∈ABy∈⦋z/x⦌B
13 4 nfel2 ⊢Ⅎxy∈⦋z/x⦌B
14 7 eleq2d ⊢x=z→y∈B↔y∈⦋z/x⦌B
15 13 14 rspce ⊢z∈A∧y∈⦋z/x⦌B→∃x∈Ay∈B
16 eliun ⊢y∈⋃x∈AB↔∃x∈Ay∈B
17 15 16 sylibr ⊢z∈A∧y∈⦋z/x⦌B→y∈⋃x∈AB
18 rspe ⊢y∈⋃x∈AB∧y∈⦋z/x⦌B→∃y∈⋃x∈ABy∈⦋z/x⦌B
19 17 18 sylancom ⊢z∈A∧y∈⦋z/x⦌B→∃y∈⋃x∈ABy∈⦋z/x⦌B
20 19 ex ⊢z∈A→y∈⦋z/x⦌B→∃y∈⋃x∈ABy∈⦋z/x⦌B
21 11 12 20 exlimd ⊢z∈A→∃yy∈⦋z/x⦌B→∃y∈⋃x∈ABy∈⦋z/x⦌B
22 10 21 biimtrid ⊢z∈A→⦋z/x⦌B≠∅→∃y∈⋃x∈ABy∈⦋z/x⦌B
23 22 ralimia ⊢∀z∈A⦋z/x⦌B≠∅→∀z∈A∃y∈⋃x∈ABy∈⦋z/x⦌B
24 9 23 sylbi ⊢∀x∈AB≠∅→∀z∈A∃y∈⋃x∈ABy∈⦋z/x⦌B
25 1 2 iunex ⊢⋃x∈AB∈V
26 eleq1 ⊢y=f⁡z→y∈⦋z/x⦌B↔f⁡z∈⦋z/x⦌B
27 1 25 26 ac6 ⊢∀z∈A∃y∈⋃x∈ABy∈⦋z/x⦌B→∃ff:A⟶⋃x∈AB∧∀z∈Af⁡z∈⦋z/x⦌B
28 ffn ⊢f:A⟶⋃x∈AB→fFnA
29 nfv ⊢Ⅎzf⁡x∈B
30 4 nfel2 ⊢Ⅎxf⁡z∈⦋z/x⦌B
31 fveq2 ⊢x=z→f⁡x=f⁡z
32 31 7 eleq12d ⊢x=z→f⁡x∈B↔f⁡z∈⦋z/x⦌B
33 29 30 32 cbvralw ⊢∀x∈Af⁡x∈B↔∀z∈Af⁡z∈⦋z/x⦌B
34 33 biimpri ⊢∀z∈Af⁡z∈⦋z/x⦌B→∀x∈Af⁡x∈B
35 28 34 anim12i ⊢f:A⟶⋃x∈AB∧∀z∈Af⁡z∈⦋z/x⦌B→fFnA∧∀x∈Af⁡x∈B
36 35 eximi ⊢∃ff:A⟶⋃x∈AB∧∀z∈Af⁡z∈⦋z/x⦌B→∃ffFnA∧∀x∈Af⁡x∈B
37 24 27 36 3syl ⊢∀x∈AB≠∅→∃ffFnA∧∀x∈Af⁡x∈B