Theorem acni

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

	Ref	Expression
Assertion	acni	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}A\wedge F:A⟶𝒫X\setminus \left\{\varnothing \right\}\right)\to \exists g\forall x\in Ag\left(x\right)\in F\left(x\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢f=F\to f\left(x\right)=F\left(x\right)$$
2	1	eleq2d	$$⊢f=F\to \left(g\left(x\right)\in f\left(x\right)\leftrightarrow g\left(x\right)\in F\left(x\right)\right)$$
3	2	ralbidv	$$⊢f=F\to \left(\forall x\in Ag\left(x\right)\in f\left(x\right)\leftrightarrow \forall x\in Ag\left(x\right)\in F\left(x\right)\right)$$
4	3	exbidv	$$⊢f=F\to \left(\exists g\forall x\in Ag\left(x\right)\in f\left(x\right)\leftrightarrow \exists g\forall x\in Ag\left(x\right)\in F\left(x\right)\right)$$
5		acnrcl	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to A\in \mathrm{V}$$
6		isacn	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}A\wedge A\in \mathrm{V}\right)\to \left(X\in \underset{\_}{\mathrm{AC}}A\leftrightarrow \forall f\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)\exists g\forall x\in Ag\left(x\right)\in f\left(x\right)\right)$$
7	5 6	mpdan	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to \left(X\in \underset{\_}{\mathrm{AC}}A\leftrightarrow \forall f\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)\exists g\forall x\in Ag\left(x\right)\in f\left(x\right)\right)$$
8	7	ibi	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to \forall f\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)\exists g\forall x\in Ag\left(x\right)\in f\left(x\right)$$
9	8	adantr	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}A\wedge F:A⟶𝒫X\setminus \left\{\varnothing \right\}\right)\to \forall f\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)\exists g\forall x\in Ag\left(x\right)\in f\left(x\right)$$
10		pwexg	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to 𝒫X\in \mathrm{V}$$
11	10	difexd	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to 𝒫X\setminus \left\{\varnothing \right\}\in \mathrm{V}$$
12	11 5	elmapd	$$⊢X\in \underset{\_}{\mathrm{AC}}A\to \left(F\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)\leftrightarrow F:A⟶𝒫X\setminus \left\{\varnothing \right\}\right)$$
13	12	biimpar	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}A\wedge F:A⟶𝒫X\setminus \left\{\varnothing \right\}\right)\to F\in \left({\left(𝒫X\setminus \left\{\varnothing \right\}\right)}^A\right)$$
14	4 9 13	rspcdva	$$⊢\left(X\in \underset{\_}{\mathrm{AC}}A\wedge F:A⟶𝒫X\setminus \left\{\varnothing \right\}\right)\to \exists g\forall x\in Ag\left(x\right)\in F\left(x\right)$$