# 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 ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)$

### Proof

Step Hyp Ref Expression
1 eldifsn ${⊢}{B}\in \left(𝒫{X}\setminus \left\{\varnothing \right\}\right)↔\left({B}\in 𝒫{X}\wedge {B}\ne \varnothing \right)$
2 elpw2g ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to \left({B}\in 𝒫{X}↔{B}\subseteq {X}\right)$
3 2 anbi1d ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to \left(\left({B}\in 𝒫{X}\wedge {B}\ne \varnothing \right)↔\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)$
4 1 3 syl5bb ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to \left({B}\in \left(𝒫{X}\setminus \left\{\varnothing \right\}\right)↔\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)$
5 4 ralbidv ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \left(𝒫{X}\setminus \left\{\varnothing \right\}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)$
6 5 biimpar ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \left(𝒫{X}\setminus \left\{\varnothing \right\}\right)$
7 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
8 7 fmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in \left(𝒫{X}\setminus \left\{\varnothing \right\}\right)↔\left({x}\in {A}⟼{B}\right):{A}⟶𝒫{X}\setminus \left\{\varnothing \right\}$
9 6 8 sylib ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \left({x}\in {A}⟼{B}\right):{A}⟶𝒫{X}\setminus \left\{\varnothing \right\}$
10 acni ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \left({x}\in {A}⟼{B}\right):{A}⟶𝒫{X}\setminus \left\{\varnothing \right\}\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)$
11 9 10 syldan ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \exists {f}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)$
12 nffvmpt1 ${⊢}\underset{_}{Ⅎ}{x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}⟼{B}\right)\left({y}\right)$
13 12 nfel2 ${⊢}Ⅎ{x}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)$
14 nfv ${⊢}Ⅎ{y}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)$
15 fveq2 ${⊢}{y}={x}\to {f}\left({y}\right)={f}\left({x}\right)$
16 fveq2 ${⊢}{y}={x}\to \left({x}\in {A}⟼{B}\right)\left({y}\right)=\left({x}\in {A}⟼{B}\right)\left({x}\right)$
17 15 16 eleq12d ${⊢}{y}={x}\to \left({f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)↔{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)$
18 13 14 17 cbvralw ${⊢}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)$
19 simplr ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)$
20 simplr ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to {x}\in {A}$
21 simpll ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to {X}\in \underset{_}{\mathrm{AC}}{A}$
22 simpr ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to {B}\subseteq {X}$
23 21 22 ssexd ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to {B}\in \mathrm{V}$
24 7 fvmpt2 ${⊢}\left({x}\in {A}\wedge {B}\in \mathrm{V}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
25 20 23 24 syl2anc ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to \left({x}\in {A}⟼{B}\right)\left({x}\right)={B}$
26 25 eleq2d ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\wedge {B}\subseteq {X}\right)\to \left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)$
27 26 ex ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\to \left({B}\subseteq {X}\to \left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)\right)$
28 27 adantrd ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge {x}\in {A}\right)\to \left(\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\to \left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)\right)$
29 28 ralimdva ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)\right)$
30 29 imp ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)$
31 ralbi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔{f}\left({x}\right)\in {B}\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
32 30 31 syl ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\right)$
33 32 biimpa ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}$
34 ssel ${⊢}{B}\subseteq {X}\to \left({f}\left({x}\right)\in {B}\to {f}\left({x}\right)\in {X}\right)$
35 34 adantr ${⊢}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\to \left({f}\left({x}\right)\in {B}\to {f}\left({x}\right)\in {X}\right)$
36 35 ral2imi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {X}\right)$
37 19 33 36 sylc ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {X}$
38 fveq2 ${⊢}{x}={y}\to {f}\left({x}\right)={f}\left({y}\right)$
39 38 eleq1d ${⊢}{x}={y}\to \left({f}\left({x}\right)\in {X}↔{f}\left({y}\right)\in {X}\right)$
40 39 rspccva ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {X}\wedge {y}\in {A}\right)\to {f}\left({y}\right)\in {X}$
41 37 40 sylan ${⊢}\left(\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\wedge {y}\in {A}\right)\to {f}\left({y}\right)\in {X}$
42 41 fmpttd ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \left({y}\in {A}⟼{f}\left({y}\right)\right):{A}⟶{X}$
43 simpll ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to {X}\in \underset{_}{\mathrm{AC}}{A}$
44 acnrcl ${⊢}{X}\in \underset{_}{\mathrm{AC}}{A}\to {A}\in \mathrm{V}$
45 43 44 syl ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to {A}\in \mathrm{V}$
46 fex2 ${⊢}\left(\left({y}\in {A}⟼{f}\left({y}\right)\right):{A}⟶{X}\wedge {A}\in \mathrm{V}\wedge {X}\in \underset{_}{\mathrm{AC}}{A}\right)\to \left({y}\in {A}⟼{f}\left({y}\right)\right)\in \mathrm{V}$
47 42 45 43 46 syl3anc ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \left({y}\in {A}⟼{f}\left({y}\right)\right)\in \mathrm{V}$
48 eqid ${⊢}\left({y}\in {A}⟼{f}\left({y}\right)\right)=\left({y}\in {A}⟼{f}\left({y}\right)\right)$
49 fvex ${⊢}{f}\left({x}\right)\in \mathrm{V}$
50 15 48 49 fvmpt ${⊢}{x}\in {A}\to \left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)={f}\left({x}\right)$
51 50 eleq1d ${⊢}{x}\in {A}\to \left(\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}↔{f}\left({x}\right)\in {B}\right)$
52 51 ralbiia ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in {B}$
53 33 52 sylibr ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}$
54 42 53 jca ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \left(\left({y}\in {A}⟼{f}\left({y}\right)\right):{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}\right)$
55 feq1 ${⊢}{g}=\left({y}\in {A}⟼{f}\left({y}\right)\right)\to \left({g}:{A}⟶{X}↔\left({y}\in {A}⟼{f}\left({y}\right)\right):{A}⟶{X}\right)$
56 fveq1 ${⊢}{g}=\left({y}\in {A}⟼{f}\left({y}\right)\right)\to {g}\left({x}\right)=\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)$
57 56 eleq1d ${⊢}{g}=\left({y}\in {A}⟼{f}\left({y}\right)\right)\to \left({g}\left({x}\right)\in {B}↔\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}\right)$
58 57 ralbidv ${⊢}{g}=\left({y}\in {A}⟼{f}\left({y}\right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}\right)$
59 55 58 anbi12d ${⊢}{g}=\left({y}\in {A}⟼{f}\left({y}\right)\right)\to \left(\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)↔\left(\left({y}\in {A}⟼{f}\left({y}\right)\right):{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {A}⟼{f}\left({y}\right)\right)\left({x}\right)\in {B}\right)\right)$
60 47 54 59 spcedv ${⊢}\left(\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)$
61 60 ex ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right)\in \left({x}\in {A}⟼{B}\right)\left({x}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)\right)$
62 18 61 syl5bi ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \left(\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)\right)$
63 62 exlimdv ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \left(\exists {f}\phantom{\rule{.4em}{0ex}}\forall {y}\in {A}\phantom{\rule{.4em}{0ex}}{f}\left({y}\right)\in \left({x}\in {A}⟼{B}\right)\left({y}\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)\right)$
64 11 63 mpd ${⊢}\left({X}\in \underset{_}{\mathrm{AC}}{A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {X}\wedge {B}\ne \varnothing \right)\right)\to \exists {g}\phantom{\rule{.4em}{0ex}}\left({g}:{A}⟶{X}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{g}\left({x}\right)\in {B}\right)$