Metamath Proof Explorer

Theorem acni2

Description: The property of being a choice set of length A . (Contributed by Mario Carneiro, 31-Aug-2015)

Ref Expression
Assertion acni2 ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∃gg:A⟶X∧∀x∈Ag⁡x∈B

Proof

Step Hyp Ref Expression
1 eldifsn ⊢B∈𝒫X∖∅↔B∈𝒫X∧B≠∅
2 elpw2g ⊢X∈AC_A→B∈𝒫X↔B⊆X
3 2 anbi1d ⊢X∈AC_A→B∈𝒫X∧B≠∅↔B⊆X∧B≠∅
4 1 3 bitrid ⊢X∈AC_A→B∈𝒫X∖∅↔B⊆X∧B≠∅
5 4 ralbidv ⊢X∈AC_A→∀x∈AB∈𝒫X∖∅↔∀x∈AB⊆X∧B≠∅
6 5 biimpar ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∀x∈AB∈𝒫X∖∅
7 eqid ⊢x∈A⟼B=x∈A⟼B
8 7 fmpt ⊢∀x∈AB∈𝒫X∖∅↔x∈A⟼B:A⟶𝒫X∖∅
9 6 8 sylib ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→x∈A⟼B:A⟶𝒫X∖∅
10 acni ⊢X∈AC_A∧x∈A⟼B:A⟶𝒫X∖∅→∃f∀y∈Af⁡y∈x∈A⟼B⁡y
11 9 10 syldan ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∃f∀y∈Af⁡y∈x∈A⟼B⁡y
12 nffvmpt1 ⊢Ⅎ_xx∈A⟼B⁡y
13 12 nfel2 ⊢Ⅎxf⁡y∈x∈A⟼B⁡y
14 nfv ⊢Ⅎyf⁡x∈x∈A⟼B⁡x
15 fveq2 ⊢y=x→f⁡y=f⁡x
16 fveq2 ⊢y=x→x∈A⟼B⁡y=x∈A⟼B⁡x
17 15 16 eleq12d ⊢y=x→f⁡y∈x∈A⟼B⁡y↔f⁡x∈x∈A⟼B⁡x
18 13 14 17 cbvralw ⊢∀y∈Af⁡y∈x∈A⟼B⁡y↔∀x∈Af⁡x∈x∈A⟼B⁡x
19 simplr ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→∀x∈AB⊆X∧B≠∅
20 simplr ⊢X∈AC_A∧x∈A∧B⊆X→x∈A
21 simpll ⊢X∈AC_A∧x∈A∧B⊆X→X∈AC_A
22 simpr ⊢X∈AC_A∧x∈A∧B⊆X→B⊆X
23 21 22 ssexd ⊢X∈AC_A∧x∈A∧B⊆X→B∈V
24 7 fvmpt2 ⊢x∈A∧B∈V→x∈A⟼B⁡x=B
25 20 23 24 syl2anc ⊢X∈AC_A∧x∈A∧B⊆X→x∈A⟼B⁡x=B
26 25 eleq2d ⊢X∈AC_A∧x∈A∧B⊆X→f⁡x∈x∈A⟼B⁡x↔f⁡x∈B
27 26 ex ⊢X∈AC_A∧x∈A→B⊆X→f⁡x∈x∈A⟼B⁡x↔f⁡x∈B
28 27 adantrd ⊢X∈AC_A∧x∈A→B⊆X∧B≠∅→f⁡x∈x∈A⟼B⁡x↔f⁡x∈B
29 28 ralimdva ⊢X∈AC_A→∀x∈AB⊆X∧B≠∅→∀x∈Af⁡x∈x∈A⟼B⁡x↔f⁡x∈B
30 29 imp ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∀x∈Af⁡x∈x∈A⟼B⁡x↔f⁡x∈B
31 ralbi ⊢∀x∈Af⁡x∈x∈A⟼B⁡x↔f⁡x∈B→∀x∈Af⁡x∈x∈A⟼B⁡x↔∀x∈Af⁡x∈B
32 30 31 syl ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∀x∈Af⁡x∈x∈A⟼B⁡x↔∀x∈Af⁡x∈B
33 32 biimpa ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→∀x∈Af⁡x∈B
34 ssel ⊢B⊆X→f⁡x∈B→f⁡x∈X
35 34 adantr ⊢B⊆X∧B≠∅→f⁡x∈B→f⁡x∈X
36 35 ral2imi ⊢∀x∈AB⊆X∧B≠∅→∀x∈Af⁡x∈B→∀x∈Af⁡x∈X
37 19 33 36 sylc ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→∀x∈Af⁡x∈X
38 fveq2 ⊢x=y→f⁡x=f⁡y
39 38 eleq1d ⊢x=y→f⁡x∈X↔f⁡y∈X
40 39 rspccva ⊢∀x∈Af⁡x∈X∧y∈A→f⁡y∈X
41 37 40 sylan ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x∧y∈A→f⁡y∈X
42 41 fmpttd ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→y∈A⟼f⁡y:A⟶X
43 simpll ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→X∈AC_A
44 acnrcl ⊢X∈AC_A→A∈V
45 43 44 syl ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→A∈V
46 fex2 ⊢y∈A⟼f⁡y:A⟶X∧A∈V∧X∈AC_A→y∈A⟼f⁡y∈V
47 42 45 43 46 syl3anc ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→y∈A⟼f⁡y∈V
48 eqid ⊢y∈A⟼f⁡y=y∈A⟼f⁡y
49 fvex ⊢f⁡x∈V
50 15 48 49 fvmpt ⊢x∈A→y∈A⟼f⁡y⁡x=f⁡x
51 50 eleq1d ⊢x∈A→y∈A⟼f⁡y⁡x∈B↔f⁡x∈B
52 51 ralbiia ⊢∀x∈Ay∈A⟼f⁡y⁡x∈B↔∀x∈Af⁡x∈B
53 33 52 sylibr ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→∀x∈Ay∈A⟼f⁡y⁡x∈B
54 42 53 jca ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→y∈A⟼f⁡y:A⟶X∧∀x∈Ay∈A⟼f⁡y⁡x∈B
55 feq1 ⊢g=y∈A⟼f⁡y→g:A⟶X↔y∈A⟼f⁡y:A⟶X
56 fveq1 ⊢g=y∈A⟼f⁡y→g⁡x=y∈A⟼f⁡y⁡x
57 56 eleq1d ⊢g=y∈A⟼f⁡y→g⁡x∈B↔y∈A⟼f⁡y⁡x∈B
58 57 ralbidv ⊢g=y∈A⟼f⁡y→∀x∈Ag⁡x∈B↔∀x∈Ay∈A⟼f⁡y⁡x∈B
59 55 58 anbi12d ⊢g=y∈A⟼f⁡y→g:A⟶X∧∀x∈Ag⁡x∈B↔y∈A⟼f⁡y:A⟶X∧∀x∈Ay∈A⟼f⁡y⁡x∈B
60 47 54 59 spcedv ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅∧∀x∈Af⁡x∈x∈A⟼B⁡x→∃gg:A⟶X∧∀x∈Ag⁡x∈B
61 60 ex ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∀x∈Af⁡x∈x∈A⟼B⁡x→∃gg:A⟶X∧∀x∈Ag⁡x∈B
62 18 61 biimtrid ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∀y∈Af⁡y∈x∈A⟼B⁡y→∃gg:A⟶X∧∀x∈Ag⁡x∈B
63 62 exlimdv ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∃f∀y∈Af⁡y∈x∈A⟼B⁡y→∃gg:A⟶X∧∀x∈Ag⁡x∈B
64 11 63 mpd ⊢X∈AC_A∧∀x∈AB⊆X∧B≠∅→∃gg:A⟶X∧∀x∈Ag⁡x∈B