Theorem ac5b 4815

Description: Equivalent of Axiom of Choice.

Hypothesis

Ref	Expression
ac5b.1	|- A e. V

Assertion

Ref	Expression
ac5b	|- (A.x e. A x =/= (/) -> E.f(f:A-->U.A /\ A.x e. A (f` x) e. x))

Distinct variable group:   x,f,A

Proof of Theorem ac5b

Step	Hyp	Ref	Expression
1		ac5b.1	. . 3 |- A e. V
2	1	ac5 4814	. 2 |- E.f(f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))
3		19.42v 1350	. . 3 |- (E.f(A.x e. A x =/= (/) /\ (f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))) <-> (A.x e. A x =/= (/) /\ E.f(f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))))
4		chfnrn 3859	. . . . . . . . . 10 |- ((f Fn A /\ A.x e. A (f` x) e. x) -> ran f (_ U.A)
5	4	ex 380	. . . . . . . . 9 |- (f Fn A -> (A.x e. A (f` x) e. x -> ran f (_ U.A))
6	5	anc2li 309	. . . . . . . 8 |- (f Fn A -> (A.x e. A (f` x) e. x -> (f Fn A /\ ran f (_ U.A)))
7		df-f 3251	. . . . . . . 8 |- (f:A-->U.A <-> (f Fn A /\ ran f (_ U.A))
8	6, 7	syl6ibr 220	. . . . . . 7 |- (f Fn A -> (A.x e. A (f` x) e. x -> f:A-->U.A))
9	8	impac 396	. . . . . 6 |- ((f Fn A /\ A.x e. A (f` x) e. x) -> (f:A-->U.A /\ A.x e. A (f` x) e. x))
10		r19.26 1797	. . . . . . 7 |- (A.x e. A (x =/= (/) /\ (x =/= (/) -> (f` x) e. x)) <-> (A.x e. A x =/= (/) /\ A.x e. A (x =/= (/) -> (f` x) e. x)))
11		pm3.35 366	. . . . . . . 8 |- ((x =/= (/) /\ (x =/= (/) -> (f` x) e. x)) -> (f` x) e. x)
12	11	r19.20si 1753	. . . . . . 7 |- (A.x e. A (x =/= (/) /\ (x =/= (/) -> (f` x) e. x)) -> A.x e. A (f` x) e. x)
13	10, 12	sylbir 208	. . . . . 6 |- ((A.x e. A x =/= (/) /\ A.x e. A (x =/= (/) -> (f` x) e. x)) -> A.x e. A (f` x) e. x)
14	9, 13	sylan2 462	. . . . 5 |- ((f Fn A /\ (A.x e. A x =/= (/) /\ A.x e. A (x =/= (/) -> (f` x) e. x))) -> (f:A-->U.A /\ A.x e. A (f` x) e. x))
15	14	an1s 497	. . . 4 |- ((A.x e. A x =/= (/) /\ (f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))) -> (f:A-->U.A /\ A.x e. A (f` x) e. x))
16	15	19.22i 1081	. . 3 |- (E.f(A.x e. A x =/= (/) /\ (f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))) -> E.f(f:A-->U.A /\ A.x e. A (f` x) e. x))
17	3, 16	sylbir 208	. 2 |- ((A.x e. A x =/= (/) /\ E.f(f Fn A /\ A.x e. A (x =/= (/) -> (f` x) e. x))) -> E.f(f:A-->U.A /\ A.x e. A (f` x) e. x))
18	2, 17	mpan2 708	1 |- (A.x e. A x =/= (/) -> E.f(f:A-->U.A /\ A.x e. A (f` x) e. x))

Syntax hints:   -> wi 3   /\ wa 230   e. wcel 999  E.wex 1021   =/= wne 1632  A.wral 1692  Vcvv 1858   (_ wss 2098  (/)c0 2331  U.cuni 2557  ran crn 3228   Fn wfn 3234  -->wf 3235  ` cfv 3239

This theorem is referenced by:  ac6lem 4816

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-9 1006  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-rep 2748  ax-sep 2758  ax-pow 2798  ax-pr 2835  ax-un 2922  ax-ac 4806

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-ral 1696  df-rex 1697  df-reu 1698  df-rab 1699  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-op 2468  df-uni 2558  df-br 2675  df-opab 2722  df-id 2891  df-xp 3241  df-rel 3242  df-cnv 3243  df-co 3244  df-dm 3245  df-rn 3246  df-res 3247  df-ima 3248  df-fun 3249  df-fn 3250  df-f 3251  df-fv 3255

Copyright terms: Public domain