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

Metamath Proof Explorer

Theorem ac6mapd

Description: Axiom of choice equivalent, deduction form. (Contributed by Thierry Arnoux, 13-Oct-2025)

Ref Expression
Hypotheses ac6mapd.1 
|- ( y = ( f ` x ) -> ( ps <-> ch ) )
ac6mapd.2 
|- ( ph -> A e. V )
ac6mapd.3 
|- ( ph -> B e. W )
ac6mapd.4 
|- ( ( ph /\ x e. A ) -> E. y e. B ps )
Assertion ac6mapd 
|- ( ph -> E. f e. ( B ^m A ) A. x e. A ch )

Proof

Step Hyp Ref Expression
1 ac6mapd.1 
 |-  ( y = ( f ` x ) -> ( ps <-> ch ) )
2 ac6mapd.2 
 |-  ( ph -> A e. V )
3 ac6mapd.3 
 |-  ( ph -> B e. W )
4 ac6mapd.4 
 |-  ( ( ph /\ x e. A ) -> E. y e. B ps )
5 4 ralrimiva 
 |-  ( ph -> A. x e. A E. y e. B ps )
6 1 ac6sg 
 |-  ( A e. V -> ( A. x e. A E. y e. B ps -> E. f ( f : A --> B /\ A. x e. A ch ) ) )
7 2 5 6 sylc 
 |-  ( ph -> E. f ( f : A --> B /\ A. x e. A ch ) )
8 3 2 elmapd 
 |-  ( ph -> ( f e. ( B ^m A ) <-> f : A --> B ) )
9 8 biimprd 
 |-  ( ph -> ( f : A --> B -> f e. ( B ^m A ) ) )
10 9 anim1d 
 |-  ( ph -> ( ( f : A --> B /\ A. x e. A ch ) -> ( f e. ( B ^m A ) /\ A. x e. A ch ) ) )
11 10 eximdv 
 |-  ( ph -> ( E. f ( f : A --> B /\ A. x e. A ch ) -> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) ) )
12 7 11 mpd 
 |-  ( ph -> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) )
13 df-rex 
 |-  ( E. f e. ( B ^m A ) A. x e. A ch <-> E. f ( f e. ( B ^m A ) /\ A. x e. A ch ) )
14 12 13 sylibr 
 |-  ( ph -> E. f e. ( B ^m A ) A. x e. A ch )