This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )