Theorem ac6sfi 6792

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 2626	. . . 4 |- ( u = (/) -> ( A. x e. u E. y e. B ph <-> A. x e. (/) E. y e. B ph ) )
2		feq2 5256	. . . . . 6 |- ( u = (/) -> ( f : u --> B <-> f : (/) --> B ) )
3		raleq 2626	. . . . . 6 |- ( u = (/) -> ( A. x e. u ps <-> A. x e. (/) ps ) )
4	2, 3	anbi12d 464	. . . . 5 |- ( u = (/) -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : (/) --> B /\ A. x e. (/) ps ) ) )
5	4	exbidv 1797	. . . 4 |- ( u = (/) -> ( E. f ( f : u --> B /\ A. x e. u ps ) <-> E. f ( f : (/) --> B /\ A. x e. (/) ps ) ) )
6	1, 5	imbi12d 233	. . 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 2626	. . . 4 |- ( u = w -> ( A. x e. u E. y e. B ph <-> A. x e. w E. y e. B ph ) )
8		feq2 5256	. . . . . 6 |- ( u = w -> ( f : u --> B <-> f : w --> B ) )
9		raleq 2626	. . . . . 6 |- ( u = w -> ( A. x e. u ps <-> A. x e. w ps ) )
10	8, 9	anbi12d 464	. . . . 5 |- ( u = w -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : w --> B /\ A. x e. w ps ) ) )
11	10	exbidv 1797	. . . 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 233	. . 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 2626	. . . 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 5256	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( f : u --> B <-> f : ( w u. { z } ) --> B ) )
15		raleq 2626	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( A. x e. u ps <-> A. x e. ( w u. { z } ) ps ) )
16	14, 15	anbi12d 464	. . . . . 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 1797	. . . . 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 5255	. . . . . . 7 |- ( f = g -> ( f : ( w u. { z } ) --> B <-> g : ( w u. { z } ) --> B ) )
19		vex 2689	. . . . . . . . . . 11 |- f e. _V
20		vex 2689	. . . . . . . . . . 11 |- x e. _V
21	19, 20	fvex 5441	. . . . . . . . . 10 |- ( f ` x ) e. _V
22		ac6sfi.1	. . . . . . . . . 10 |- ( y = ( f ` x ) -> ( ph <-> ps ) )
23	21, 22	sbcie 2943	. . . . . . . . 9 |- ( [. ( f ` x ) / y ]. ph <-> ps )
24		fveq1 5420	. . . . . . . . . 10 |- ( f = g -> ( f ` x ) = ( g ` x ) )
25	24	sbceq1d 2914	. . . . . . . . 9 |- ( f = g -> ( [. ( f ` x ) / y ]. ph <-> [. ( g ` x ) / y ]. ph ) )
26	23, 25	syl5bbr 193	. . . . . . . 8 |- ( f = g -> ( ps <-> [. ( g ` x ) / y ]. ph ) )
27	26	ralbidv 2437	. . . . . . 7 |- ( f = g -> ( A. x e. ( w u. { z } ) ps <-> A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
28	18, 27	anbi12d 464	. . . . . 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 1890	. . . . 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	syl6bb 195	. . . 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 233	. . 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 2626	. . . 4 |- ( u = A -> ( A. x e. u E. y e. B ph <-> A. x e. A E. y e. B ph ) )
33		feq2 5256	. . . . . 6 |- ( u = A -> ( f : u --> B <-> f : A --> B ) )
34		raleq 2626	. . . . . 6 |- ( u = A -> ( A. x e. u ps <-> A. x e. A ps ) )
35	33, 34	anbi12d 464	. . . . 5 |- ( u = A -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) )
36	35	exbidv 1797	. . . 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 233	. . 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 5313	. . . 4 |- (/) : (/) --> B
39		0ex 4055	. . . . 5 |- (/) e. _V
40		ral0 3464	. . . . . . 7 |- A. x e. (/) ps
41	40	biantru 300	. . . . . 6 |- ( f : (/) --> B <-> ( f : (/) --> B /\ A. x e. (/) ps ) )
42		feq1 5255	. . . . . 6 |- ( f = (/) -> ( f : (/) --> B <-> (/) : (/) --> B ) )
43	41, 42	syl5bbr 193	. . . . 5 |- ( f = (/) -> ( ( f : (/) --> B /\ A. x e. (/) ps ) <-> (/) : (/) --> B ) )
44	39, 43	spcev 2780	. . . 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 3239	. . . . . . 7 |- w C_ ( w u. { z } )
47		ssralv 3161	. . . . . . 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 3240	. . . . . . . . 9 |- { z } C_ ( w u. { z } )
51		ssralv 3161	. . . . . . . . 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 2689	. . . . . . . . . 10 |- z e. _V
54		ralsnsg 3561	. . . . . . . . . 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 2988	. . . . . . . . 9 |- ( [. z / x ]. E. y e. B ph <-> E. y e. B [. z / x ]. ph )
57	55, 56	bitri 183	. . . . . . . 8 |- ( A. x e. { z } E. y e. B ph <-> E. y e. B [. z / x ]. ph )
58	52, 57	sylib 121	. . . . . . 7 |- ( A. x e. ( w u. { z } ) E. y e. B ph -> E. y e. B [. z / x ]. ph )
59		nfv 1508	. . . . . . . 8 |- F/ y -. z e. w
60		nfv 1508	. . . . . . . . 9 |- F/ y E. f ( f : w --> B /\ A. x e. w ps )
61		nfv 1508	. . . . . . . . . . 11 |- F/ y g : ( w u. { z } ) --> B
62		nfcv 2281	. . . . . . . . . . . 12 |- F/_ y ( w u. { z } )
63		nfsbc1v 2927	. . . . . . . . . . . 12 |- F/ y [. ( g ` x ) / y ]. ph
64	62, 63	nfralxy 2471	. . . . . . . . . . 11 |- F/ y A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph
65	61, 64	nfan 1544	. . . . . . . . . 10 |- F/ y ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
66	65	nfex 1616	. . . . . . . . 9 |- F/ y E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
67	60, 66	nfim 1551	. . . . . . . 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 520	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> f : w --> B )
69		vex 2689	. . . . . . . . . . . . . . . 16 |- y e. _V
70	53, 69	f1osn 5407	. . . . . . . . . . . . . . 15 |- { <. z , y >. } : { z } -1-1-onto-> { y }
71		f1of 5367	. . . . . . . . . . . . . . 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 985	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y e. B )
74	73	snssd 3665	. . . . . . . . . . . . . 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 5285	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> B )
76		simpl1 984	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> -. z e. w )
77		disjsn 3585	. . . . . . . . . . . . . 14 |- ( ( w i^i { z } ) = (/) <-> -. z e. w )
78	76, 77	sylibr 133	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> ( w i^i { z } ) = (/) )
79		fun2 5296	. . . . . . . . . . . . 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 1215	. . . . . . . . . . . 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 521	. . . . . . . . . . . . . 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 2211	. . . . . . . . . . . . . . . . . . 19 |- ( x e. w -> ( z = x -> z e. w ) )
83	82	necon3bd 2351	. . . . . . . . . . . . . . . . . 18 |- ( x e. w -> ( -. z e. w -> z =/= x ) )
84	83	impcom 124	. . . . . . . . . . . . . . . . 17 |- ( ( -. z e. w /\ x e. w ) -> z =/= x )
85		fvunsng 5614	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. _V /\ z =/= x ) -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
86	20, 85	mpan 420	. . . . . . . . . . . . . . . . 17 |- ( z =/= x -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
87		dfsbcq 2911	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) -> ( [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph <-> [. ( f ` x ) / y ]. ph ) )
88	87, 23	syl6rbb 196	. . . . . . . . . . . . . . . . 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 2433	. . . . . . . . . . . . . . 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 146	. . . . . . . . . . . . 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 986	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> [. z / x ]. ph )
94		ffun 5275	. . . . . . . . . . . . . . . . 17 |- ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B -> Fun ( f u. { <. z , y >. } ) )
95		ssun2 3240	. . . . . . . . . . . . . . . . . 18 |- { <. z , y >. } C_ ( f u. { <. z , y >. } )
96		vsnid 3557	. . . . . . . . . . . . . . . . . . 19 |- z e. { z }
97	69	dmsnop 5012	. . . . . . . . . . . . . . . . . . 19 |- dom { <. z , y >. } = { z }
98	96, 97	eleqtrri 2215	. . . . . . . . . . . . . . . . . 18 |- z e. dom { <. z , y >. }
99		funssfv 5447	. . . . . . . . . . . . . . . . . 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 1307	. . . . . . . . . . . . . . . . 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 5615	. . . . . . . . . . . . . . . 16 |- ( { <. z , y >. } ` z ) = y
103	101, 102	syl6req 2189	. . . . . . . . . . . . . . 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 3561	. . . . . . . . . . . . . . . . 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 3545	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { z } -> x = z )
107	106	fveq2d 5425	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. { z } -> ( ( f u. { <. z , y >. } ) ` x ) = ( ( f u. { <. z , y >. } ) ` z ) )
108	107	eqeq2d 2151	. . . . . . . . . . . . . . . . . . 19 |- ( x e. { z } -> ( y = ( ( f u. { <. z , y >. } ) ` x ) <-> y = ( ( f u. { <. z , y >. } ) ` z ) ) )
109	108	biimparc 297	. . . . . . . . . . . . . . . . . 18 |- ( ( y = ( ( f u. { <. z , y >. } ) ` z ) /\ x e. { z } ) -> y = ( ( f u. { <. z , y >. } ) ` x ) )
110		sbceq1a 2918	. . . . . . . . . . . . . . . . . 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 2433	. . . . . . . . . . . . . . . 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	syl5bbr 193	. . . . . . . . . . . . . . 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 146	. . . . . . . . . . . . 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 3258	. . . . . . . . . . . . 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 408	. . . . . . . . . . . 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 4151	. . . . . . . . . . . . . . 15 |- <. z , y >. e. _V
119	118	snex 4109	. . . . . . . . . . . . . 14 |- { <. z , y >. } e. _V
120	19, 119	unex 4362	. . . . . . . . . . . . 13 |- ( f u. { <. z , y >. } ) e. _V
121		feq1 5255	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( g : ( w u. { z } ) --> B <-> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B ) )
122		fveq1 5420	. . . . . . . . . . . . . . . 16 |- ( g = ( f u. { <. z , y >. } ) -> ( g ` x ) = ( ( f u. { <. z , y >. } ) ` x ) )
123	122	sbceq1d 2914	. . . . . . . . . . . . . . 15 |- ( g = ( f u. { <. z , y >. } ) -> ( [. ( g ` x ) / y ]. ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
124	123	ralbidv 2437	. . . . . . . . . . . . . 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 464	. . . . . . . . . . . . 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 2780	. . . . . . . . . . . 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 408	. . . . . . . . . . 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 114	. . . . . . . . . 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 1791	. . . . . . . . 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 1180	. . . . . . . 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 2546	. . . . . . 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 275	. . 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 6784	. 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 123	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 103   <-> wb 104   /\ w3a 962   = wceq 1331   E.wex 1468   e. wcel 1480   =/= wne 2308   A.wral 2416   E.wrex 2417   _Vcvv 2686   [.wsbc 2909   u. cun 3069   i^i cin 3070   C_ wss 3071   (/)c0 3363   {csn 3527   <.cop 3530   dom cdm 4539   Fun wfun 5117   -->wf 5119   -1-1-onto->wf1o 5122   ` cfv 5123   Fincfn 6634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-coll 4043  ax-sep 4046  ax-nul 4054  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-iinf 4502

This theorem depends on definitions:  df-bi 116  df-dc 820  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-ral 2421  df-rex 2422  df-reu 2423  df-rab 2425  df-v 2688  df-sbc 2910  df-csb 3004  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-nul 3364  df-if 3475  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-iun 3815  df-br 3930  df-opab 3990  df-mpt 3991  df-tr 4027  df-id 4215  df-iord 4288  df-on 4290  df-suc 4293  df-iom 4505  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-rn 4550  df-res 4551  df-ima 4552  df-iota 5088  df-fun 5125  df-fn 5126  df-f 5127  df-f1 5128  df-fo 5129  df-f1o 5130  df-fv 5131  df-er 6429  df-en 6635  df-fin 6637

This theorem is referenced by: (None)