Theorem axccd2

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

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

Proof

Step	Hyp	Ref	Expression
1		axccd2.1	|- ( ph -> A ~<_ _om )
2		axccd2.2	|- ( ( ph /\ x e. A ) -> x =/= (/) )
3		isfinite2	|- ( A ~< _om -> A e. Fin )
4	3	adantl	|- ( ( ph /\ A ~< _om ) -> A e. Fin )
5		simpr	|- ( ( ( ph /\ A ~< _om ) /\ x e. A ) -> x e. A )
6	2	adantlr	|- ( ( ( ph /\ A ~< _om ) /\ x e. A ) -> x =/= (/) )
7	4 5 6	choicefi	|- ( ( ph /\ A ~< _om ) -> E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) )
8		simpr	|- ( ( f Fn A /\ A. x e. A ( f ` x ) e. x ) -> A. x e. A ( f ` x ) e. x )
9	8	a1i	|- ( ( ph /\ A ~< _om ) -> ( ( f Fn A /\ A. x e. A ( f ` x ) e. x ) -> A. x e. A ( f ` x ) e. x ) )
10	9	eximdv	|- ( ( ph /\ A ~< _om ) -> ( E. f ( f Fn A /\ A. x e. A ( f ` x ) e. x ) -> E. f A. x e. A ( f ` x ) e. x ) )
11	7 10	mpd	|- ( ( ph /\ A ~< _om ) -> E. f A. x e. A ( f ` x ) e. x )
12	1	anim1i	|- ( ( ph /\ -. A ~< _om ) -> ( A ~<_ _om /\ -. A ~< _om ) )
13		bren2	|- ( A ~~ _om <-> ( A ~<_ _om /\ -. A ~< _om ) )
14	12 13	sylibr	|- ( ( ph /\ -. A ~< _om ) -> A ~~ _om )
15		simpr	|- ( ( ph /\ A ~~ _om ) -> A ~~ _om )
16	2	adantlr	|- ( ( ( ph /\ A ~~ _om ) /\ x e. A ) -> x =/= (/) )
17	15 16	axccd	|- ( ( ph /\ A ~~ _om ) -> E. f A. x e. A ( f ` x ) e. x )
18	14 17	syldan	|- ( ( ph /\ -. A ~< _om ) -> E. f A. x e. A ( f ` x ) e. x )
19	11 18	pm2.61dan	|- ( ph -> E. f A. x e. A ( f ` x ) e. x )