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

Metamath Proof Explorer

Theorem axccd

Description: An alternative version of the axiom of countable choice. (Contributed by Glauco Siliprandi, 26-Jun-2021)

Ref Expression
Hypotheses axccd.1 
|- ( ph -> A ~~ _om )
axccd.2 
|- ( ( ph /\ x e. A ) -> x =/= (/) )
Assertion axccd 
|- ( ph -> E. f A. x e. A ( f ` x ) e. x )

Proof

Step Hyp Ref Expression
1 axccd.1 
 |-  ( ph -> A ~~ _om )
2 axccd.2 
 |-  ( ( ph /\ x e. A ) -> x =/= (/) )
3 encv 
 |-  ( A ~~ _om -> ( A e. _V /\ _om e. _V ) )
4 3 simpld 
 |-  ( A ~~ _om -> A e. _V )
5 breq1 
 |-  ( y = A -> ( y ~~ _om <-> A ~~ _om ) )
6 raleq 
 |-  ( y = A -> ( A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) <-> A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
7 6 exbidv 
 |-  ( y = A -> ( E. f A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) <-> E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
8 5 7 imbi12d 
 |-  ( y = A -> ( ( y ~~ _om -> E. f A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) ) <-> ( A ~~ _om -> E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) ) )
9 ax-cc 
 |-  ( y ~~ _om -> E. f A. x e. y ( x =/= (/) -> ( f ` x ) e. x ) )
10 8 9 vtoclg 
 |-  ( A e. _V -> ( A ~~ _om -> E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
11 1 4 10 3syl 
 |-  ( ph -> ( A ~~ _om -> E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) )
12 1 11 mpd 
 |-  ( ph -> E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) )
13 nfv 
 |-  F/ x ph
14 nfra1 
 |-  F/ x A. x e. A ( x =/= (/) -> ( f ` x ) e. x )
15 13 14 nfan 
 |-  F/ x ( ph /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) )
16 2 adantlr 
 |-  ( ( ( ph /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. A ) -> x =/= (/) )
17 rspa 
 |-  ( ( A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) /\ x e. A ) -> ( x =/= (/) -> ( f ` x ) e. x ) )
18 17 adantll 
 |-  ( ( ( ph /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. A ) -> ( x =/= (/) -> ( f ` x ) e. x ) )
19 16 18 mpd 
 |-  ( ( ( ph /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) /\ x e. A ) -> ( f ` x ) e. x )
20 15 19 ralrimia 
 |-  ( ( ph /\ A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) ) -> A. x e. A ( f ` x ) e. x )
21 20 ex 
 |-  ( ph -> ( A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) -> A. x e. A ( f ` x ) e. x ) )
22 21 eximdv 
 |-  ( ph -> ( E. f A. x e. A ( x =/= (/) -> ( f ` x ) e. x ) -> E. f A. x e. A ( f ` x ) e. x ) )
23 12 22 mpd 
 |-  ( ph -> E. f A. x e. A ( f ` x ) e. x )