Theorem ac6sfi 6959

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 2693	. . . 4 |- ( u = (/) -> ( A. x e. u E. y e. B ph <-> A. x e. (/) E. y e. B ph ) )
2		feq2 5391	. . . . . 6 |- ( u = (/) -> ( f : u --> B <-> f : (/) --> B ) )
3		raleq 2693	. . . . . 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 1839	. . . 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 2693	. . . 4 |- ( u = w -> ( A. x e. u E. y e. B ph <-> A. x e. w E. y e. B ph ) )
8		feq2 5391	. . . . . 6 |- ( u = w -> ( f : u --> B <-> f : w --> B ) )
9		raleq 2693	. . . . . 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 1839	. . . 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 2693	. . . 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 5391	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( f : u --> B <-> f : ( w u. { z } ) --> B ) )
15		raleq 2693	. . . . . . 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 1839	. . . . 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 5390	. . . . . . 7 |- ( f = g -> ( f : ( w u. { z } ) --> B <-> g : ( w u. { z } ) --> B ) )
19		vex 2766	. . . . . . . . . . 11 |- f e. _V
20		vex 2766	. . . . . . . . . . 11 |- x e. _V
21	19, 20	fvex 5578	. . . . . . . . . 10 |- ( f ` x ) e. _V
22		ac6sfi.1	. . . . . . . . . 10 |- ( y = ( f ` x ) -> ( ph <-> ps ) )
23	21, 22	sbcie 3024	. . . . . . . . 9 |- ( [. ( f ` x ) / y ]. ph <-> ps )
24		fveq1 5557	. . . . . . . . . 10 |- ( f = g -> ( f ` x ) = ( g ` x ) )
25	24	sbceq1d 2994	. . . . . . . . 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 2497	. . . . . . 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 1933	. . . . 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 2693	. . . 4 |- ( u = A -> ( A. x e. u E. y e. B ph <-> A. x e. A E. y e. B ph ) )
33		feq2 5391	. . . . . 6 |- ( u = A -> ( f : u --> B <-> f : A --> B ) )
34		raleq 2693	. . . . . 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 1839	. . . 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 5448	. . . 4 |- (/) : (/) --> B
39		0ex 4160	. . . . 5 |- (/) e. _V
40		ral0 3552	. . . . . . 7 |- A. x e. (/) ps
41	40	biantru 302	. . . . . 6 |- ( f : (/) --> B <-> ( f : (/) --> B /\ A. x e. (/) ps ) )
42		feq1 5390	. . . . . 6 |- ( f = (/) -> ( f : (/) --> B <-> (/) : (/) --> B ) )
43	41, 42	bitr3id 194	. . . . 5 |- ( f = (/) -> ( ( f : (/) --> B /\ A. x e. (/) ps ) <-> (/) : (/) --> B ) )
44	39, 43	spcev 2859	. . . 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 3326	. . . . . . 7 |- w C_ ( w u. { z } )
47		ssralv 3247	. . . . . . 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 3327	. . . . . . . . 9 |- { z } C_ ( w u. { z } )
51		ssralv 3247	. . . . . . . . 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 2766	. . . . . . . . . 10 |- z e. _V
54		ralsnsg 3659	. . . . . . . . . 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 3069	. . . . . . . . 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 1542	. . . . . . . 8 |- F/ y -. z e. w
60		nfv 1542	. . . . . . . . 9 |- F/ y E. f ( f : w --> B /\ A. x e. w ps )
61		nfv 1542	. . . . . . . . . . 11 |- F/ y g : ( w u. { z } ) --> B
62		nfcv 2339	. . . . . . . . . . . 12 |- F/_ y ( w u. { z } )
63		nfsbc1v 3008	. . . . . . . . . . . 12 |- F/ y [. ( g ` x ) / y ]. ph
64	62, 63	nfralxy 2535	. . . . . . . . . . 11 |- F/ y A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph
65	61, 64	nfan 1579	. . . . . . . . . 10 |- F/ y ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
66	65	nfex 1651	. . . . . . . . 9 |- F/ y E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
67	60, 66	nfim 1586	. . . . . . . 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 529	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> f : w --> B )
69		vex 2766	. . . . . . . . . . . . . . . 16 |- y e. _V
70	53, 69	f1osn 5544	. . . . . . . . . . . . . . 15 |- { <. z , y >. } : { z } -1-1-onto-> { y }
71		f1of 5504	. . . . . . . . . . . . . . 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 1003	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y e. B )
74	73	snssd 3767	. . . . . . . . . . . . . 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 5420	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> B )
76		simpl1 1002	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> -. z e. w )
77		disjsn 3684	. . . . . . . . . . . . . 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 5431	. . . . . . . . . . . . 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 1248	. . . . . . . . . . . 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 531	. . . . . . . . . . . . . 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 2268	. . . . . . . . . . . . . . . . . . 19 |- ( x e. w -> ( z = x -> z e. w ) )
83	82	necon3bd 2410	. . . . . . . . . . . . . . . . . 18 |- ( x e. w -> ( -. z e. w -> z =/= x ) )
84	83	impcom 125	. . . . . . . . . . . . . . . . 17 |- ( ( -. z e. w /\ x e. w ) -> z =/= x )
85		fvunsng 5756	. . . . . . . . . . . . . . . . . 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 2991	. . . . . . . . . . . . . . . . . 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 2493	. . . . . . . . . . . . . . 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 1004	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> [. z / x ]. ph )
94		ffun 5410	. . . . . . . . . . . . . . . . 17 |- ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B -> Fun ( f u. { <. z , y >. } ) )
95		ssun2 3327	. . . . . . . . . . . . . . . . . 18 |- { <. z , y >. } C_ ( f u. { <. z , y >. } )
96		vsnid 3654	. . . . . . . . . . . . . . . . . . 19 |- z e. { z }
97	69	dmsnop 5143	. . . . . . . . . . . . . . . . . . 19 |- dom { <. z , y >. } = { z }
98	96, 97	eleqtrri 2272	. . . . . . . . . . . . . . . . . 18 |- z e. dom { <. z , y >. }
99		funssfv 5584	. . . . . . . . . . . . . . . . . 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 1340	. . . . . . . . . . . . . . . . 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 5757	. . . . . . . . . . . . . . . 16 |- ( { <. z , y >. } ` z ) = y
103	101, 102	eqtr2di 2246	. . . . . . . . . . . . . . 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 3659	. . . . . . . . . . . . . . . . 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 3640	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { z } -> x = z )
107	106	fveq2d 5562	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. { z } -> ( ( f u. { <. z , y >. } ) ` x ) = ( ( f u. { <. z , y >. } ) ` z ) )
108	107	eqeq2d 2208	. . . . . . . . . . . . . . . . . . 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 2999	. . . . . . . . . . . . . . . . . 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 2493	. . . . . . . . . . . . . . . 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 3345	. . . . . . . . . . . . 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 4262	. . . . . . . . . . . . . . 15 |- <. z , y >. e. _V
119	118	snex 4218	. . . . . . . . . . . . . 14 |- { <. z , y >. } e. _V
120	19, 119	unex 4476	. . . . . . . . . . . . 13 |- ( f u. { <. z , y >. } ) e. _V
121		feq1 5390	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( g : ( w u. { z } ) --> B <-> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B ) )
122		fveq1 5557	. . . . . . . . . . . . . . . 16 |- ( g = ( f u. { <. z , y >. } ) -> ( g ` x ) = ( ( f u. { <. z , y >. } ) ` x ) )
123	122	sbceq1d 2994	. . . . . . . . . . . . . . 15 |- ( g = ( f u. { <. z , y >. } ) -> ( [. ( g ` x ) / y ]. ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
124	123	ralbidv 2497	. . . . . . . . . . . . . 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 2859	. . . . . . . . . . . 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 1833	. . . . . . . . 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 1204	. . . . . . . 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 2611	. . . . . . 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 6951	. 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 980   = wceq 1364   E.wex 1506   e. wcel 2167   =/= wne 2367   A.wral 2475   E.wrex 2476   _Vcvv 2763   [.wsbc 2989   u. cun 3155   i^i cin 3156   C_ wss 3157   (/)c0 3450   {csn 3622   <.cop 3625   dom cdm 4663   Fun wfun 5252   -->wf 5254   -1-1-onto->wf1o 5257   ` cfv 5258   Fincfn 6799

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 615  ax-in2 616  ax-io 710  ax-5 1461  ax-7 1462  ax-gen 1463  ax-ie1 1507  ax-ie2 1508  ax-8 1518  ax-10 1519  ax-11 1520  ax-i12 1521  ax-bndl 1523  ax-4 1524  ax-17 1540  ax-i9 1544  ax-ial 1548  ax-i5r 1549  ax-13 2169  ax-14 2170  ax-ext 2178  ax-coll 4148  ax-sep 4151  ax-nul 4159  ax-pow 4207  ax-pr 4242  ax-un 4468  ax-setind 4573  ax-iinf 4624

This theorem depends on definitions:  df-bi 117  df-dc 836  df-3or 981  df-3an 982  df-tru 1367  df-fal 1370  df-nf 1475  df-sb 1777  df-eu 2048  df-mo 2049  df-clab 2183  df-cleq 2189  df-clel 2192  df-nfc 2328  df-ne 2368  df-ral 2480  df-rex 2481  df-reu 2482  df-rab 2484  df-v 2765  df-sbc 2990  df-csb 3085  df-dif 3159  df-un 3161  df-in 3163  df-ss 3170  df-nul 3451  df-if 3562  df-pw 3607  df-sn 3628  df-pr 3629  df-op 3631  df-uni 3840  df-int 3875  df-iun 3918  df-br 4034  df-opab 4095  df-mpt 4096  df-tr 4132  df-id 4328  df-iord 4401  df-on 4403  df-suc 4406  df-iom 4627  df-xp 4669  df-rel 4670  df-cnv 4671  df-co 4672  df-dm 4673  df-rn 4674  df-res 4675  df-ima 4676  df-iota 5219  df-fun 5260  df-fn 5261  df-f 5262  df-f1 5263  df-fo 5264  df-f1o 5265  df-fv 5266  df-er 6592  df-en 6800  df-fin 6802

This theorem is referenced by: (None)