Theorem ac6n

Description: Equivalent of Axiom of Choice. Contrapositive of ac6s . (Contributed by NM, 10-Jun-2007)

	Ref	Expression
Hypotheses	ac6s.1	$$⊢A\in \mathrm{V}$$
	ac6s.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
Assertion	ac6n	$$⊢\forall f\left(f:A⟶B\to \exists x\in A\psi \right)\to \exists x\in A\forall y\in B\phi$$

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	$$⊢A\in \mathrm{V}$$
2		ac6s.2	$$⊢y=f\left(x\right)\to \left(\phi \leftrightarrow \psi \right)$$
3	2	notbid	$$⊢y=f\left(x\right)\to \left(\neg \phi \leftrightarrow \neg \psi \right)$$
4	1 3	ac6s	$$⊢\forall x\in A\exists y\in B\neg \phi \to \exists f\left(f:A⟶B\wedge \forall x\in A\neg \psi \right)$$
5	4	con3i	$$⊢\neg \exists f\left(f:A⟶B\wedge \forall x\in A\neg \psi \right)\to \neg \forall x\in A\exists y\in B\neg \phi$$
6		dfrex2	$$⊢\exists x\in A\psi \leftrightarrow \neg \forall x\in A\neg \psi$$
7	6	imbi2i	$$⊢\left(f:A⟶B\to \exists x\in A\psi \right)\leftrightarrow \left(f:A⟶B\to \neg \forall x\in A\neg \psi \right)$$
8	7	albii	$$⊢\forall f\left(f:A⟶B\to \exists x\in A\psi \right)\leftrightarrow \forall f\left(f:A⟶B\to \neg \forall x\in A\neg \psi \right)$$
9		alinexa	$$⊢\forall f\left(f:A⟶B\to \neg \forall x\in A\neg \psi \right)\leftrightarrow \neg \exists f\left(f:A⟶B\wedge \forall x\in A\neg \psi \right)$$
10	8 9	bitri	$$⊢\forall f\left(f:A⟶B\to \exists x\in A\psi \right)\leftrightarrow \neg \exists f\left(f:A⟶B\wedge \forall x\in A\neg \psi \right)$$
11		dfral2	$$⊢\forall y\in B\phi \leftrightarrow \neg \exists y\in B\neg \phi$$
12	11	rexbii	$$⊢\exists x\in A\forall y\in B\phi \leftrightarrow \exists x\in A\neg \exists y\in B\neg \phi$$
13		rexnal	$$⊢\exists x\in A\neg \exists y\in B\neg \phi \leftrightarrow \neg \forall x\in A\exists y\in B\neg \phi$$
14	12 13	bitri	$$⊢\exists x\in A\forall y\in B\phi \leftrightarrow \neg \forall x\in A\exists y\in B\neg \phi$$
15	5 10 14	3imtr4i	$$⊢\forall f\left(f:A⟶B\to \exists x\in A\psi \right)\to \exists x\in A\forall y\in B\phi$$