Theorem ac6sfi 7202

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 2749	. . . 4 |- ( u = (/) -> ( A. x e. u E. y e. B ph <-> A. x e. (/) E. y e. B ph ) )
2		feq2 5517	. . . . . 6 |- ( u = (/) -> ( f : u --> B <-> f : (/) --> B ) )
3		raleq 2749	. . . . . 6 |- ( u = (/) -> ( A. x e. u ps <-> A. x e. (/) ps ) )
4	2, 3	anbi12d 477	. . . . 5 |- ( u = (/) -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : (/) --> B /\ A. x e. (/) ps ) ) )
5	4	exbidv 1878	. . . 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 2749	. . . 4 |- ( u = w -> ( A. x e. u E. y e. B ph <-> A. x e. w E. y e. B ph ) )
8		feq2 5517	. . . . . 6 |- ( u = w -> ( f : u --> B <-> f : w --> B ) )
9		raleq 2749	. . . . . 6 |- ( u = w -> ( A. x e. u ps <-> A. x e. w ps ) )
10	8, 9	anbi12d 477	. . . . 5 |- ( u = w -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : w --> B /\ A. x e. w ps ) ) )
11	10	exbidv 1878	. . . 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 2749	. . . 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 5517	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( f : u --> B <-> f : ( w u. { z } ) --> B ) )
15		raleq 2749	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( A. x e. u ps <-> A. x e. ( w u. { z } ) ps ) )
16	14, 15	anbi12d 477	. . . . . 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 1878	. . . . 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 5516	. . . . . . 7 |- ( f = g -> ( f : ( w u. { z } ) --> B <-> g : ( w u. { z } ) --> B ) )
19		vex 2824	. . . . . . . . . . 11 |- f e. _V
20		vex 2824	. . . . . . . . . . 11 |- x e. _V
21	19, 20	fvex 5715	. . . . . . . . . 10 |- ( f ` x ) e. _V
22		ac6sfi.1	. . . . . . . . . 10 |- ( y = ( f ` x ) -> ( ph <-> ps ) )
23	21, 22	sbcie 3086	. . . . . . . . 9 |- ( [. ( f ` x ) / y ]. ph <-> ps )
24		fveq1 5694	. . . . . . . . . 10 |- ( f = g -> ( f ` x ) = ( g ` x ) )
25	24	sbceq1d 3056	. . . . . . . . 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 2550	. . . . . . 7 |- ( f = g -> ( A. x e. ( w u. { z } ) ps <-> A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
28	18, 27	anbi12d 477	. . . . . 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 1974	. . . . 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 2749	. . . 4 |- ( u = A -> ( A. x e. u E. y e. B ph <-> A. x e. A E. y e. B ph ) )
33		feq2 5517	. . . . . 6 |- ( u = A -> ( f : u --> B <-> f : A --> B ) )
34		raleq 2749	. . . . . 6 |- ( u = A -> ( A. x e. u ps <-> A. x e. A ps ) )
35	33, 34	anbi12d 477	. . . . 5 |- ( u = A -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) )
36	35	exbidv 1878	. . . 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 5583	. . . 4 |- (/) : (/) --> B
39		0ex 4260	. . . . 5 |- (/) e. _V
40		ral0 3629	. . . . . . 7 |- A. x e. (/) ps
41	40	biantru 302	. . . . . 6 |- ( f : (/) --> B <-> ( f : (/) --> B /\ A. x e. (/) ps ) )
42		feq1 5516	. . . . . 6 |- ( f = (/) -> ( f : (/) --> B <-> (/) : (/) --> B ) )
43	41, 42	bitr3id 194	. . . . 5 |- ( f = (/) -> ( ( f : (/) --> B /\ A. x e. (/) ps ) <-> (/) : (/) --> B ) )
44	39, 43	spcev 2920	. . . 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 3392	. . . . . . 7 |- w C_ ( w u. { z } )
47		ssralv 3312	. . . . . . 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 3393	. . . . . . . . 9 |- { z } C_ ( w u. { z } )
51		ssralv 3312	. . . . . . . . 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 2824	. . . . . . . . . 10 |- z e. _V
54		ralsnsg 3746	. . . . . . . . . 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 3131	. . . . . . . . 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 1581	. . . . . . . 8 |- F/ y -. z e. w
60		nfv 1581	. . . . . . . . 9 |- F/ y E. f ( f : w --> B /\ A. x e. w ps )
61		nfv 1581	. . . . . . . . . . 11 |- F/ y g : ( w u. { z } ) --> B
62		nfcv 2392	. . . . . . . . . . . 12 |- F/_ y ( w u. { z } )
63		nfsbc1v 3070	. . . . . . . . . . . 12 |- F/ y [. ( g ` x ) / y ]. ph
64	62, 63	nfralxy 2588	. . . . . . . . . . 11 |- F/ y A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph
65	61, 64	nfan 1618	. . . . . . . . . 10 |- F/ y ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
66	65	nfex 1690	. . . . . . . . 9 |- F/ y E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
67	60, 66	nfim 1625	. . . . . . . 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 535	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> f : w --> B )
69		vex 2824	. . . . . . . . . . . . . . . 16 |- y e. _V
70	53, 69	f1osn 5681	. . . . . . . . . . . . . . 15 |- { <. z , y >. } : { z } -1-1-onto-> { y }
71		f1of 5639	. . . . . . . . . . . . . . 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 1032	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y e. B )
74	73	snssd 3860	. . . . . . . . . . . . . 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 5547	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> B )
76		simpl1 1031	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> -. z e. w )
77		disjsn 3771	. . . . . . . . . . . . . 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 5562	. . . . . . . . . . . . 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 1277	. . . . . . . . . . . 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 537	. . . . . . . . . . . . . 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 2310	. . . . . . . . . . . . . . . . . . 19 |- ( x e. w -> ( z = x -> z e. w ) )
83	82	necon3bd 2463	. . . . . . . . . . . . . . . . . 18 |- ( x e. w -> ( -. z e. w -> z =/= x ) )
84	83	impcom 125	. . . . . . . . . . . . . . . . 17 |- ( ( -. z e. w /\ x e. w ) -> z =/= x )
85		fvunsng 5909	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. _V /\ z =/= x ) -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
86	20, 85	mpan 428	. . . . . . . . . . . . . . . . 17 |- ( z =/= x -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
87		dfsbcq 3053	. . . . . . . . . . . . . . . . . 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 2546	. . . . . . . . . . . . . . 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 1033	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> [. z / x ]. ph )
94		ffun 5536	. . . . . . . . . . . . . . . . 17 |- ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B -> Fun ( f u. { <. z , y >. } ) )
95		ssun2 3393	. . . . . . . . . . . . . . . . . 18 |- { <. z , y >. } C_ ( f u. { <. z , y >. } )
96		vsnid 3741	. . . . . . . . . . . . . . . . . . 19 |- z e. { z }
97	69	dmsnop 5261	. . . . . . . . . . . . . . . . . . 19 |- dom { <. z , y >. } = { z }
98	96, 97	eleqtrri 2314	. . . . . . . . . . . . . . . . . 18 |- z e. dom { <. z , y >. }
99		funssfv 5721	. . . . . . . . . . . . . . . . . 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 1370	. . . . . . . . . . . . . . . . 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 5910	. . . . . . . . . . . . . . . 16 |- ( { <. z , y >. } ` z ) = y
103	101, 102	eqtr2di 2288	. . . . . . . . . . . . . . 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 3746	. . . . . . . . . . . . . . . . 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 3727	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { z } -> x = z )
107	106	fveq2d 5699	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. { z } -> ( ( f u. { <. z , y >. } ) ` x ) = ( ( f u. { <. z , y >. } ) ` z ) )
108	107	eqeq2d 2250	. . . . . . . . . . . . . . . . . . 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 3061	. . . . . . . . . . . . . . . . . 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 2546	. . . . . . . . . . . . . . . 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 3411	. . . . . . . . . . . . 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 415	. . . . . . . . . . . 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 4369	. . . . . . . . . . . . . . 15 |- <. z , y >. e. _V
119	118	snex 4322	. . . . . . . . . . . . . 14 |- { <. z , y >. } e. _V
120	19, 119	unex 4587	. . . . . . . . . . . . 13 |- ( f u. { <. z , y >. } ) e. _V
121		feq1 5516	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( g : ( w u. { z } ) --> B <-> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B ) )
122		fveq1 5694	. . . . . . . . . . . . . . . 16 |- ( g = ( f u. { <. z , y >. } ) -> ( g ` x ) = ( ( f u. { <. z , y >. } ) ` x ) )
123	122	sbceq1d 3056	. . . . . . . . . . . . . . 15 |- ( g = ( f u. { <. z , y >. } ) -> ( [. ( g ` x ) / y ]. ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
124	123	ralbidv 2550	. . . . . . . . . . . . . 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 477	. . . . . . . . . . . . 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 2920	. . . . . . . . . . . 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 415	. . . . . . . . . . 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 1872	. . . . . . . . 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 1233	. . . . . . . 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 2665	. . . . . . 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 7194	. 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 ) )

This proof depends on syntax axioms:   -. wn 3   -> wi 4   /\ wa 104   <-> wb 105   /\ w3a 1009   = wceq 1402   E.wex 1545   e. wcel 2209   =/= wne 2420   A.wral 2528   E.wrex 2529   _Vcvv 2821   [.wsbc 3051   u. cun 3218   i^i cin 3219   C_ wss 3220   (/)c0 3520   {csn 3709   <.cop 3712   dom cdm 4774   Fun wfun 5371   -->wf 5373   -1-1-onto->wf1o 5376   ` cfv 5377   Fincfn 7022

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-coll 4246  ax-sep 4249  ax-nul 4259  ax-pow 4311  ax-pr 4346  ax-un 4578  ax-setind 4684  ax-iinf 4735

This proof depends on definitions:  df-bi 117  df-dc 847  df-3or 1010  df-3an 1011  df-tru 1405  df-fal 1408  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-reu 2535  df-rab 2537  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-int 3971  df-iun 4014  df-br 4131  df-opab 4193  df-mpt 4194  df-tr 4230  df-id 4438  df-iord 4511  df-on 4513  df-suc 4516  df-iom 4738  df-xp 4780  df-rel 4781  df-cnv 4782  df-co 4783  df-dm 4784  df-rn 4785  df-res 4786  df-ima 4787  df-iota 5337  df-fun 5379  df-fn 5380  df-f 5381  df-f1 5382  df-fo 5383  df-f1o 5384  df-fv 5385  df-er 6807  df-en 7023  df-fin 7025

This theorem is used by:  finacn  7560