Theorem ac6n

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

	Ref	Expression
Hypotheses	ac6s.1	|- A e. _V
	ac6s.2	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
Assertion	ac6n	|- ( A. f ( f : A --> B -> E. x e. A ps ) -> E. x e. A A. y e. B ph )

Proof

Step	Hyp	Ref	Expression
1		ac6s.1	|- A e. _V
2		ac6s.2	|- ( y = ( f ` x ) -> ( ph <-> ps ) )
3	2	notbid	|- ( y = ( f ` x ) -> ( -. ph <-> -. ps ) )
4	1 3	ac6s	|- ( A. x e. A E. y e. B -. ph -> E. f ( f : A --> B /\ A. x e. A -. ps ) )
5	4	con3i	|- ( -. E. f ( f : A --> B /\ A. x e. A -. ps ) -> -. A. x e. A E. y e. B -. ph )
6		dfrex2	|- ( E. x e. A ps <-> -. A. x e. A -. ps )
7	6	imbi2i	|- ( ( f : A --> B -> E. x e. A ps ) <-> ( f : A --> B -> -. A. x e. A -. ps ) )
8	7	albii	|- ( A. f ( f : A --> B -> E. x e. A ps ) <-> A. f ( f : A --> B -> -. A. x e. A -. ps ) )
9		alinexa	|- ( A. f ( f : A --> B -> -. A. x e. A -. ps ) <-> -. E. f ( f : A --> B /\ A. x e. A -. ps ) )
10	8 9	bitri	|- ( A. f ( f : A --> B -> E. x e. A ps ) <-> -. E. f ( f : A --> B /\ A. x e. A -. ps ) )
11		dfral2	|- ( A. y e. B ph <-> -. E. y e. B -. ph )
12	11	rexbii	|- ( E. x e. A A. y e. B ph <-> E. x e. A -. E. y e. B -. ph )
13		rexnal	|- ( E. x e. A -. E. y e. B -. ph <-> -. A. x e. A E. y e. B -. ph )
14	12 13	bitri	|- ( E. x e. A A. y e. B ph <-> -. A. x e. A E. y e. B -. ph )
15	5 10 14	3imtr4i	|- ( A. f ( f : A --> B -> E. x e. A ps ) -> E. x e. A A. y e. B ph )