Theorem dfac11

Description: The right-hand side of this theorem (compare with ac4 ), sometimes known as the "axiom of multiple choice", is a choice equivalent. Curiously, this statement cannot be proved without ax-reg , despite not mentioning the cumulative hierarchy in any way as most consequences of regularity do.

This is definition (MC) of Schechter p. 141.EDITORIAL: the proof is not original with me of course but I lost my reference sometime after writing it.

A multiple choice function allows any total order to be extended to a choice function, which in turn defines a well-ordering. Since a well-ordering on a set defines a simple ordering of the power set, this allows the trivial well-ordering of the empty set to be transfinitely bootstrapped up the cumulative hierarchy to any desired level. (Contributed by Stefan O'Rear, 20-Jan-2015) (Revised by Stefan O'Rear, 1-Jun-2015)

	Ref	Expression
Assertion	dfac11	|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfac3	|- ( CHOICE <-> A. a E. c A. d e. a ( d =/= (/) -> ( c ` d ) e. d ) )
2		raleq	|- ( a = x -> ( A. d e. a ( d =/= (/) -> ( c ` d ) e. d ) <-> A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) ) )
3	2	exbidv	|- ( a = x -> ( E. c A. d e. a ( d =/= (/) -> ( c ` d ) e. d ) <-> E. c A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) ) )
4	3	cbvalvw	|- ( A. a E. c A. d e. a ( d =/= (/) -> ( c ` d ) e. d ) <-> A. x E. c A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) )
5		neeq1	|- ( d = z -> ( d =/= (/) <-> z =/= (/) ) )
6		fveq2	|- ( d = z -> ( c ` d ) = ( c ` z ) )
7		id	|- ( d = z -> d = z )
8	6 7	eleq12d	|- ( d = z -> ( ( c ` d ) e. d <-> ( c ` z ) e. z ) )
9	5 8	imbi12d	|- ( d = z -> ( ( d =/= (/) -> ( c ` d ) e. d ) <-> ( z =/= (/) -> ( c ` z ) e. z ) ) )
10	9	cbvralvw	|- ( A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) <-> A. z e. x ( z =/= (/) -> ( c ` z ) e. z ) )
11		fveq2	|- ( b = z -> ( c ` b ) = ( c ` z ) )
12	11	sneqd	|- ( b = z -> { ( c ` b ) } = { ( c ` z ) } )
13		eqid	|- ( b e. x |-> { ( c ` b ) } ) = ( b e. x |-> { ( c ` b ) } )
14		snex	|- { ( c ` z ) } e. _V
15	12 13 14	fvmpt	|- ( z e. x -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) = { ( c ` z ) } )
16	15	3ad2ant1	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) = { ( c ` z ) } )
17		simp3	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> ( c ` z ) e. z )
18	17	snssd	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } C_ z )
19	14	elpw	|- ( { ( c ` z ) } e. ~P z <-> { ( c ` z ) } C_ z )
20	18 19	sylibr	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } e. ~P z )
21		snfi	|- { ( c ` z ) } e. Fin
22	21	a1i	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } e. Fin )
23	20 22	elind	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } e. ( ~P z i^i Fin ) )
24		fvex	|- ( c ` z ) e. _V
25	24	snnz	|- { ( c ` z ) } =/= (/)
26	25	a1i	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } =/= (/) )
27		eldifsn	|- ( { ( c ` z ) } e. ( ( ~P z i^i Fin ) \ { (/) } ) <-> ( { ( c ` z ) } e. ( ~P z i^i Fin ) /\ { ( c ` z ) } =/= (/) ) )
28	23 26 27	sylanbrc	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> { ( c ` z ) } e. ( ( ~P z i^i Fin ) \ { (/) } ) )
29	16 28	eqeltrd	|- ( ( z e. x /\ z =/= (/) /\ ( c ` z ) e. z ) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) )
30	29	3exp	|- ( z e. x -> ( z =/= (/) -> ( ( c ` z ) e. z -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
31	30	a2d	|- ( z e. x -> ( ( z =/= (/) -> ( c ` z ) e. z ) -> ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
32	31	ralimia	|- ( A. z e. x ( z =/= (/) -> ( c ` z ) e. z ) -> A. z e. x ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
33	10 32	sylbi	|- ( A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) -> A. z e. x ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
34		vex	|- x e. _V
35	34	mptex	|- ( b e. x |-> { ( c ` b ) } ) e. _V
36		fveq1	|- ( f = ( b e. x |-> { ( c ` b ) } ) -> ( f ` z ) = ( ( b e. x |-> { ( c ` b ) } ) ` z ) )
37	36	eleq1d	|- ( f = ( b e. x |-> { ( c ` b ) } ) -> ( ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) <-> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
38	37	imbi2d	|- ( f = ( b e. x |-> { ( c ` b ) } ) -> ( ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) <-> ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
39	38	ralbidv	|- ( f = ( b e. x |-> { ( c ` b ) } ) -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) <-> A. z e. x ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
40	35 39	spcev	|- ( A. z e. x ( z =/= (/) -> ( ( b e. x |-> { ( c ` b ) } ) ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
41	33 40	syl	|- ( A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
42	41	exlimiv	|- ( E. c A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) -> E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
43	42	alimi	|- ( A. x E. c A. d e. x ( d =/= (/) -> ( c ` d ) e. d ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
44	4 43	sylbi	|- ( A. a E. c A. d e. a ( d =/= (/) -> ( c ` d ) e. d ) -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
45	1 44	sylbi	|- ( CHOICE -> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
46		fvex	|- ( R1 ` ( rank ` a ) ) e. _V
47	46	pwex	|- ~P ( R1 ` ( rank ` a ) ) e. _V
48		raleq	|- ( x = ~P ( R1 ` ( rank ` a ) ) -> ( A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) <-> A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
49	48	exbidv	|- ( x = ~P ( R1 ` ( rank ` a ) ) -> ( E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) <-> E. f A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) ) )
50	47 49	spcv	|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> E. f A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
51		rankon	|- ( rank ` a ) e. On
52	51	a1i	|- ( A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> ( rank ` a ) e. On )
53		id	|- ( A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )
54	52 53	aomclem8	|- ( A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> E. b b We ( R1 ` ( rank ` a ) ) )
55	54	exlimiv	|- ( E. f A. z e. ~P ( R1 ` ( rank ` a ) ) ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> E. b b We ( R1 ` ( rank ` a ) ) )
56		vex	|- a e. _V
57		r1rankid	|- ( a e. _V -> a C_ ( R1 ` ( rank ` a ) ) )
58		wess	|- ( a C_ ( R1 ` ( rank ` a ) ) -> ( b We ( R1 ` ( rank ` a ) ) -> b We a ) )
59	58	eximdv	|- ( a C_ ( R1 ` ( rank ` a ) ) -> ( E. b b We ( R1 ` ( rank ` a ) ) -> E. b b We a ) )
60	56 57 59	mp2b	|- ( E. b b We ( R1 ` ( rank ` a ) ) -> E. b b We a )
61	50 55 60	3syl	|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> E. b b We a )
62	61	alrimiv	|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> A. a E. b b We a )
63		dfac8	|- ( CHOICE <-> A. a E. b b We a )
64	62 63	sylibr	|- ( A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) -> CHOICE )
65	45 64	impbii	|- ( CHOICE <-> A. x E. f A. z e. x ( z =/= (/) -> ( f ` z ) e. ( ( ~P z i^i Fin ) \ { (/) } ) ) )