Theorem ac6sfi 7130

Description: Existence of a choice function for finite sets. (Contributed by Jeff Hankins, 26-Jun-2009.) (Proof shortened by Mario Carneiro, 29-Jan-2014.)

Hypothesis

Ref	Expression
ac6sfi.1	|- ( y = ( f ` x ) -> ( ph <-> ps ) )

Assertion

Ref	Expression
ac6sfi	|- ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )

Distinct variable groups:   x, f, A   y, f, B, x   ph, f   ps, y

Allowed substitution hints:   ph( x, y)   ps( x, f)   A( y)

Proof of Theorem ac6sfi

Dummy variables u w z g are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		raleq 2731	. . . 4 |- ( u = (/) -> ( A. x e. u E. y e. B ph <-> A. x e. (/) E. y e. B ph ) )
2		feq2 5473	. . . . . 6 |- ( u = (/) -> ( f : u --> B <-> f : (/) --> B ) )
3		raleq 2731	. . . . . 6 |- ( u = (/) -> ( A. x e. u ps <-> A. x e. (/) ps ) )
4	2, 3	anbi12d 473	. . . . 5 |- ( u = (/) -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : (/) --> B /\ A. x e. (/) ps ) ) )
5	4	exbidv 1873	. . . 4 |- ( u = (/) -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. f ( f : (/) --> B /\ A. x e. (/) ps ) ) )
6	1, 5	imbi12d 234	. . 3 |- ( u = (/) -> ( ( A. x e. u E. y e. B ph -> E. f ( f : u --> B /\ A. x e. u ps ) ) <-> ( A. x e. (/) E. y e. B ph -> E. f ( f : (/) --> B /\ A. x e. (/) ps ) ) ) )
7		raleq 2731	. . . 4 |- ( u = w -> ( A. x e. u E. y e. B ph <-> A. x e. w E. y e. B ph ) )
8		feq2 5473	. . . . . 6 |- ( u = w -> ( f : u --> B <-> f : w --> B ) )
9		raleq 2731	. . . . . 6 |- ( u = w -> ( A. x e. u ps <-> A. x e. w ps ) )
10	8, 9	anbi12d 473	. . . . 5 |- ( u = w -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : w --> B /\ A. x e. w ps ) ) )
11	10	exbidv 1873	. . . 4 |- ( u = w -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. f ( f : w --> B /\ A. x e. w ps ) ) )
12	7, 11	imbi12d 234	. . 3 |- ( u = w -> ( ( A. x e. u E. y e. B ph -> E. f ( f : u --> B /\ A. x e. u ps ) ) <-> ( A. x e. w E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) ) )
13		raleq 2731	. . . 4 |- ( u = ( w u. { z } ) -> ( A. x e. u E. y e. B ph <-> A. x e. ( w u. { z } ) E. y e. B ph ) )
14		feq2 5473	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( f : u --> B <-> f : ( w u. { z } ) --> B ) )
15		raleq 2731	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( A. x e. u ps <-> A. x e. ( w u. { z } ) ps ) )
16	14, 15	anbi12d 473	. . . . . 6 |- ( u = ( w u. { z } ) -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) ps ) ) )
17	16	exbidv 1873	. . . . 5 |- ( u = ( w u. { z } ) -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. f ( f : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) ps ) ) )
18		feq1 5472	. . . . . . 7 |- ( f = g -> ( f : ( w u. { z } ) --> B <-> g : ( w u. { z } ) --> B ) )
19		vex 2806	. . . . . . . . . . 11 |- f e. _V
20		vex 2806	. . . . . . . . . . 11 |- x e. _V
21	19, 20	fvex 5668	. . . . . . . . . 10 |- ( f ` x ) e. _V
22		ac6sfi.1	. . . . . . . . . 10 |- ( y = ( f ` x ) -> ( ph <-> ps ) )
23	21, 22	sbcie 3067	. . . . . . . . 9 |- ( [. ( f ` x ) / y ]. ph <-> ps )
24		fveq1 5647	. . . . . . . . . 10 |- ( f = g -> ( f ` x ) = ( g ` x ) )
25	24	sbceq1d 3037	. . . . . . . . 9 |- ( f = g -> ( [. ( f ` x ) / y ]. ph <-> [. ( g ` x ) / y ]. ph ) )
26	23, 25	bitr3id 194	. . . . . . . 8 |- ( f = g -> ( ps <-> [. ( g ` x ) / y ]. ph ) )
27	26	ralbidv 2533	. . . . . . 7 |- ( f = g -> ( A. x e. ( w u. { z } ) ps <-> A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
28	18, 27	anbi12d 473	. . . . . 6 |- ( f = g -> ( ( f : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) ps ) <-> ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) )
29	28	cbvexv 1967	. . . . 5 |- ( E. f ( f : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) ps ) <-> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
30	17, 29	bitrdi 196	. . . 4 |- ( u = ( w u. { z } ) -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) )
31	13, 30	imbi12d 234	. . 3 |- ( u = ( w u. { z } ) -> ( ( A. x e. u E. y e. B ph -> E. f ( f : u --> B /\ A. x e. u ps ) ) <-> ( A. x e. ( w u. { z } ) E. y e. B ph -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
32		raleq 2731	. . . 4 |- ( u = A -> ( A. x e. u E. y e. B ph <-> A. x e. A E. y e. B ph ) )
33		feq2 5473	. . . . . 6 |- ( u = A -> ( f : u --> B <-> f : A --> B ) )
34		raleq 2731	. . . . . 6 |- ( u = A -> ( A. x e. u ps <-> A. x e. A ps ) )
35	33, 34	anbi12d 473	. . . . 5 |- ( u = A -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) )
36	35	exbidv 1873	. . . 4 |- ( u = A -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. f ( f : A --> B /\ A. x e. A ps ) ) )
37	32, 36	imbi12d 234	. . 3 |- ( u = A -> ( ( A. x e. u E. y e. B ph -> E. f ( f : u --> B /\ A. x e. u ps ) ) <-> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) ) )
38		f0 5536	. . . 4 |- (/) : (/) --> B
39		0ex 4221	. . . . 5 |- (/) e. _V
40		ral0 3598	. . . . . . 7 |- A. x e. (/) ps
41	40	biantru 302	. . . . . 6 |- ( f : (/) --> B <-> ( f : (/) --> B /\ A. x e. (/) ps ) )
42		feq1 5472	. . . . . 6 |- ( f = (/) -> ( f : (/) --> B <-> (/) : (/) --> B ) )
43	41, 42	bitr3id 194	. . . . 5 |- ( f = (/) -> ( ( f : (/) --> B /\ A. x e. (/) ps ) <-> (/) : (/) --> B ) )
44	39, 43	spcev 2902	. . . 4 |- ( (/) : (/) --> B -> E. f ( f : (/) --> B /\ A. x e. (/) ps ) )
45	38, 44	mp1i 10	. . 3 |- ( A. x e. (/) E. y e. B ph -> E. f ( f : (/) --> B /\ A. x e. (/) ps ) )
46		ssun1 3372	. . . . . . 7 |- w C_ ( w u. { z } )
47		ssralv 3292	. . . . . . 7 |- ( w C_ ( w u. { z } ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> A. x e. w E. y e. B ph ) )
48	46, 47	ax-mp 5	. . . . . 6 |- ( A. x e. ( w u. { z } ) E. y e. B ph -> A. x e. w E. y e. B ph )
49	48	imim1i 60	. . . . 5 |- ( ( A. x e. w E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) )
50		ssun2 3373	. . . . . . . . 9 |- { z } C_ ( w u. { z } )
51		ssralv 3292	. . . . . . . . 9 |- ( { z } C_ ( w u. { z } ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> A. x e. { z } E. y e. B ph ) )
52	50, 51	ax-mp 5	. . . . . . . 8 |- ( A. x e. ( w u. { z } ) E. y e. B ph -> A. x e. { z } E. y e. B ph )
53		vex 2806	. . . . . . . . . 10 |- z e. _V
54		ralsnsg 3710	. . . . . . . . . 10 |- ( z e. _V -> ( A. x e. { z } E. y e. B ph <-> [. z / x ]. E. y e. B ph ) )
55	53, 54	ax-mp 5	. . . . . . . . 9 |- ( A. x e. { z } E. y e. B ph <-> [. z / x ]. E. y e. B ph )
56		sbcrex 3112	. . . . . . . . 9 |- ( [. z / x ]. E. y e. B ph <-> E. y e. B [. z / x ]. ph )
57	55, 56	bitri 184	. . . . . . . 8 |- ( A. x e. { z } E. y e. B ph <-> E. y e. B [. z / x ]. ph )
58	52, 57	sylib 122	. . . . . . 7 |- ( A. x e. ( w u. { z } ) E. y e. B ph -> E. y e. B [. z / x ]. ph )
59		nfv 1577	. . . . . . . 8 |- F/ y -. z e. w
60		nfv 1577	. . . . . . . . 9 |- F/ y E. f ( f : w --> B /\ A. x e. w ps )
61		nfv 1577	. . . . . . . . . . 11 |- F/ y g : ( w u. { z } ) --> B
62		nfcv 2375	. . . . . . . . . . . 12 |- F/_ y ( w u. { z } )
63		nfsbc1v 3051	. . . . . . . . . . . 12 |- F/ y [. ( g ` x ) / y ]. ph
64	62, 63	nfralxy 2571	. . . . . . . . . . 11 |- F/ y A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph
65	61, 64	nfan 1614	. . . . . . . . . 10 |- F/ y ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
66	65	nfex 1686	. . . . . . . . 9 |- F/ y E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
67	60, 66	nfim 1621	. . . . . . . 8 |- F/ y ( E. f ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
68		simprl 531	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> f : w --> B )
69		vex 2806	. . . . . . . . . . . . . . . 16 |- y e. _V
70	53, 69	f1osn 5634	. . . . . . . . . . . . . . 15 |- { <. z , y >. } : { z } -1-1-onto-> { y }
71		f1of 5592	. . . . . . . . . . . . . . 15 |- ( { <. z , y >. } : { z } -1-1-onto-> { y } -> { <. z , y >. } : { z } --> { y } )
72	70, 71	mp1i 10	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> { y } )
73		simpl2 1028	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y e. B )
74	73	snssd 3823	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { y } C_ B )
75	72, 74	fssd 5502	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> B )
76		simpl1 1027	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> -. z e. w )
77		disjsn 3735	. . . . . . . . . . . . . 14 |- ( ( w i^i { z } ) = (/) <-> -. z e. w )
78	76, 77	sylibr 134	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( w i^i { z } ) = (/) )
79		fun2 5517	. . . . . . . . . . . . 13 |- ( ( ( f : w --> B /\ { <. z , y >. } : { z } --> B ) /\ ( w i^i { z } ) = (/) ) -> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B )
80	68, 75, 78, 79	syl21anc 1273	. . . . . . . . . . . 12 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B )
81		simprr 533	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> A. x e. w ps )
82		eleq1a 2303	. . . . . . . . . . . . . . . . . . 19 |- ( x e. w -> ( z = x -> z e. w ) )
83	82	necon3bd 2446	. . . . . . . . . . . . . . . . . 18 |- ( x e. w -> ( -. z e. w -> z =/= x ) )
84	83	impcom 125	. . . . . . . . . . . . . . . . 17 |- ( ( -. z e. w /\ x e. w ) -> z =/= x )
85		fvunsng 5856	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. _V /\ z =/= x ) -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
86	20, 85	mpan 424	. . . . . . . . . . . . . . . . 17 |- ( z =/= x -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
87		dfsbcq 3034	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) -> ( [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph <-> [. ( f ` x ) / y ]. ph ) )
88	87, 23	bitr2di 197	. . . . . . . . . . . . . . . . 17 |- ( ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) -> ( ps <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
89	84, 86, 88	3syl 17	. . . . . . . . . . . . . . . 16 |- ( ( -. z e. w /\ x e. w ) -> ( ps <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
90	89	ralbidva 2529	. . . . . . . . . . . . . . 15 |- ( -. z e. w -> ( A. x e. w ps <-> A. x e. w [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
91	76, 90	syl 14	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( A. x e. w ps <-> A. x e. w [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
92	81, 91	mpbid 147	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> A. x e. w [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph )
93		simpl3 1029	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> [. z / x ]. ph )
94		ffun 5492	. . . . . . . . . . . . . . . . 17 |- ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B -> Fun ( f u. { <. z , y >. } ) )
95		ssun2 3373	. . . . . . . . . . . . . . . . . 18 |- { <. z , y >. } C_ ( f u. { <. z , y >. } )
96		vsnid 3705	. . . . . . . . . . . . . . . . . . 19 |- z e. { z }
97	69	dmsnop 5217	. . . . . . . . . . . . . . . . . . 19 |- dom { <. z , y >. } = { z }
98	96, 97	eleqtrri 2307	. . . . . . . . . . . . . . . . . 18 |- z e. dom { <. z , y >. }
99		funssfv 5674	. . . . . . . . . . . . . . . . . 18 |- ( ( Fun ( f u. { <. z , y >. } ) /\ { <. z , y >. } C_ ( f u. { <. z , y >. } ) /\ z e. dom { <. z , y >. } ) -> ( ( f u. { <. z , y >. } ) ` z ) = ( { <. z , y >. } ` z ) )
100	95, 98, 99	mp3an23 1366	. . . . . . . . . . . . . . . . 17 |- ( Fun ( f u. { <. z , y >. } ) -> ( ( f u. { <. z , y >. } ) ` z ) = ( { <. z , y >. } ` z ) )
101	80, 94, 100	3syl 17	. . . . . . . . . . . . . . . 16 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( ( f u. { <. z , y >. } ) ` z ) = ( { <. z , y >. } ` z ) )
102	53, 69	fvsn 5857	. . . . . . . . . . . . . . . 16 |- ( { <. z , y >. } ` z ) = y
103	101, 102	eqtr2di 2281	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y = ( ( f u. { <. z , y >. } ) ` z ) )
104		ralsnsg 3710	. . . . . . . . . . . . . . . . 17 |- ( z e. _V -> ( A. x e. { z } ph <-> [. z / x ]. ph ) )
105	53, 104	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( A. x e. { z } ph <-> [. z / x ]. ph )
106		elsni 3691	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { z } -> x = z )
107	106	fveq2d 5652	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. { z } -> ( ( f u. { <. z , y >. } ) ` x ) = ( ( f u. { <. z , y >. } ) ` z ) )
108	107	eqeq2d 2243	. . . . . . . . . . . . . . . . . . 19 |- ( x e. { z } -> ( y = ( ( f u. { <. z , y >. } ) ` x ) <-> y = ( ( f u. { <. z , y >. } ) ` z ) ) )
109	108	biimparc 299	. . . . . . . . . . . . . . . . . 18 |- ( ( y = ( ( f u. { <. z , y >. } ) ` z ) /\ x e. { z } ) -> y = ( ( f u. { <. z , y >. } ) ` x ) )
110		sbceq1a 3042	. . . . . . . . . . . . . . . . . 18 |- ( y = ( ( f u. { <. z , y >. } ) ` x ) -> ( ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
111	109, 110	syl 14	. . . . . . . . . . . . . . . . 17 |- ( ( y = ( ( f u. { <. z , y >. } ) ` z ) /\ x e. { z } ) -> ( ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
112	111	ralbidva 2529	. . . . . . . . . . . . . . . 16 |- ( y = ( ( f u. { <. z , y >. } ) ` z ) -> ( A. x e. { z } ph <-> A. x e. { z } [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
113	105, 112	bitr3id 194	. . . . . . . . . . . . . . 15 |- ( y = ( ( f u. { <. z , y >. } ) ` z ) -> ( [. z / x ]. ph <-> A. x e. { z } [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
114	103, 113	syl 14	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( [. z / x ]. ph <-> A. x e. { z } [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
115	93, 114	mpbid 147	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> A. x e. { z } [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph )
116		ralun 3391	. . . . . . . . . . . . 13 |- ( ( A. x e. w [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph /\ A. x e. { z } [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) -> A. x e. ( w u. { z } ) [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph )
117	92, 115, 116	syl2anc 411	. . . . . . . . . . . 12 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> A. x e. ( w u. { z } ) [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph )
118	53, 69	opex 4327	. . . . . . . . . . . . . . 15 |- <. z , y >. e. _V
119	118	snex 4281	. . . . . . . . . . . . . 14 |- { <. z , y >. } e. _V
120	19, 119	unex 4544	. . . . . . . . . . . . 13 |- ( f u. { <. z , y >. } ) e. _V
121		feq1 5472	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( g : ( w u. { z } ) --> B <-> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B ) )
122		fveq1 5647	. . . . . . . . . . . . . . . 16 |- ( g = ( f u. { <. z , y >. } ) -> ( g ` x ) = ( ( f u. { <. z , y >. } ) ` x ) )
123	122	sbceq1d 3037	. . . . . . . . . . . . . . 15 |- ( g = ( f u. { <. z , y >. } ) -> ( [. ( g ` x ) / y ]. ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
124	123	ralbidv 2533	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph <-> A. x e. ( w u. { z } ) [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
125	121, 124	anbi12d 473	. . . . . . . . . . . . 13 |- ( g = ( f u. { <. z , y >. } ) -> ( ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) <-> ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) ) )
126	120, 125	spcev 2902	. . . . . . . . . . . 12 |- ( ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
127	80, 117, 126	syl2anc 411	. . . . . . . . . . 11 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
128	127	ex 115	. . . . . . . . . 10 |- ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) -> ( ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) )
129	128	exlimdv 1867	. . . . . . . . 9 |- ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) -> ( E. f ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) )
130	129	3exp 1229	. . . . . . . 8 |- ( -. z e. w -> ( y e. B -> ( [. z / x ]. ph -> ( E. f ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) ) )
131	59, 67, 130	rexlimd 2648	. . . . . . 7 |- ( -. z e. w -> ( E. y e. B [. z / x ]. ph -> ( E. f ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
132	58, 131	syl5 32	. . . . . 6 |- ( -. z e. w -> ( A. x e. ( w u. { z } ) E. y e. B ph -> ( E. f ( f : w --> B /\ A. x e. w ps ) -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
133	132	a2d 26	. . . . 5 |- ( -. z e. w -> ( ( A. x e. ( w u. { z } ) E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
134	49, 133	syl5 32	. . . 4 |- ( -. z e. w -> ( ( A. x e. w E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
135	134	adantl 277	. . 3 |- ( ( w e. Fin /\ -. z e. w ) -> ( ( A. x e. w E. y e. B ph -> E. f ( f : w --> B /\ A. x e. w ps ) ) -> ( A. x e. ( w u. { z } ) E. y e. B ph -> E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) ) ) )
136	6, 12, 31, 37, 45, 135	findcard2s 7122	. 2 |- ( A e. Fin -> ( A. x e. A E. y e. B ph -> E. f ( f : A --> B /\ A. x e. A ps ) ) )
137	136	imp 124	1 |- ( ( A e. Fin /\ A. x e. A E. y e. B ph ) -> E. f ( f : A --> B /\ A. x e. A ps ) )

Syntax hints:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1005   = wceq 1398   E.wex 1541   e. wcel 2202   =/= wne 2403   A.wral 2511   E.wrex 2512   _Vcvv 2803   [.wsbc 3032   u. cun 3199   i^i cin 3200   C_ wss 3201   (/)c0 3496   {csn 3673   <.cop 3676   dom cdm 4731   Fun wfun 5327   -->wf 5329   -1-1-onto->wf1o 5332   ` cfv 5333   Fincfn 6952

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 619  ax-in2 620  ax-io 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-13 2204  ax-14 2205  ax-ext 2213  ax-coll 4209  ax-sep 4212  ax-nul 4220  ax-pow 4270  ax-pr 4305  ax-un 4536  ax-setind 4641  ax-iinf 4692

This theorem depends on definitions:  df-bi 117  df-dc 843  df-3or 1006  df-3an 1007  df-tru 1401  df-fal 1404  df-nf 1510  df-sb 1811  df-eu 2082  df-mo 2083  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2364  df-ne 2404  df-ral 2516  df-rex 2517  df-reu 2518  df-rab 2520  df-v 2805  df-sbc 3033  df-csb 3129  df-dif 3203  df-un 3205  df-in 3207  df-ss 3214  df-nul 3497  df-if 3608  df-pw 3658  df-sn 3679  df-pr 3680  df-op 3682  df-uni 3899  df-int 3934  df-iun 3977  df-br 4094  df-opab 4156  df-mpt 4157  df-tr 4193  df-id 4396  df-iord 4469  df-on 4471  df-suc 4474  df-iom 4695  df-xp 4737  df-rel 4738  df-cnv 4739  df-co 4740  df-dm 4741  df-rn 4742  df-res 4743  df-ima 4744  df-iota 5293  df-fun 5335  df-fn 5336  df-f 5337  df-f1 5338  df-fo 5339  df-f1o 5340  df-fv 5341  df-er 6745  df-en 6953  df-fin 6955

This theorem is referenced by:  finacn  7479