Theorem ac6sfi 6876

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 2665	. . . 4 |- ( u = (/) -> ( A. x e. u E. y e. B ph <-> A. x e. (/) E. y e. B ph ) )
2		feq2 5331	. . . . . 6 |- ( u = (/) -> ( f : u --> B <-> f : (/) --> B ) )
3		raleq 2665	. . . . . 6 |- ( u = (/) -> ( A. x e. u ps <-> A. x e. (/) ps ) )
4	2, 3	anbi12d 470	. . . . 5 |- ( u = (/) -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : (/) --> B /\ A. x e. (/) ps ) ) )
5	4	exbidv 1818	. . . 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 2665	. . . 4 |- ( u = w -> ( A. x e. u E. y e. B ph <-> A. x e. w E. y e. B ph ) )
8		feq2 5331	. . . . . 6 |- ( u = w -> ( f : u --> B <-> f : w --> B ) )
9		raleq 2665	. . . . . 6 |- ( u = w -> ( A. x e. u ps <-> A. x e. w ps ) )
10	8, 9	anbi12d 470	. . . . 5 |- ( u = w -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : w --> B /\ A. x e. w ps ) ) )
11	10	exbidv 1818	. . . 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 2665	. . . 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 5331	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( f : u --> B <-> f : ( w u. { z } ) --> B ) )
15		raleq 2665	. . . . . . 7 |- ( u = ( w u. { z } ) -> ( A. x e. u ps <-> A. x e. ( w u. { z } ) ps ) )
16	14, 15	anbi12d 470	. . . . . 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 1818	. . . . 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 5330	. . . . . . 7 |- ( f = g -> ( f : ( w u. { z } ) --> B <-> g : ( w u. { z } ) --> B ) )
19		vex 2733	. . . . . . . . . . 11 |- f e. _V
20		vex 2733	. . . . . . . . . . 11 |- x e. _V
21	19, 20	fvex 5516	. . . . . . . . . 10 |- ( f ` x ) e. _V
22		ac6sfi.1	. . . . . . . . . 10 |- ( y = ( f ` x ) -> ( ph <-> ps ) )
23	21, 22	sbcie 2989	. . . . . . . . 9 |- ( [. ( f ` x ) / y ]. ph <-> ps )
24		fveq1 5495	. . . . . . . . . 10 |- ( f = g -> ( f ` x ) = ( g ` x ) )
25	24	sbceq1d 2960	. . . . . . . . 9 |- ( f = g -> ( [. ( f ` x ) / y ]. ph <-> [. ( g ` x ) / y ]. ph ) )
26	23, 25	bitr3id 193	. . . . . . . 8 |- ( f = g -> ( ps <-> [. ( g ` x ) / y ]. ph ) )
27	26	ralbidv 2470	. . . . . . 7 |- ( f = g -> ( A. x e. ( w u. { z } ) ps <-> A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph ) )
28	18, 27	anbi12d 470	. . . . . 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 1911	. . . . 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 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 2665	. . . 4 |- ( u = A -> ( A. x e. u E. y e. B ph <-> A. x e. A E. y e. B ph ) )
33		feq2 5331	. . . . . 6 |- ( u = A -> ( f : u --> B <-> f : A --> B ) )
34		raleq 2665	. . . . . 6 |- ( u = A -> ( A. x e. u ps <-> A. x e. A ps ) )
35	33, 34	anbi12d 470	. . . . 5 |- ( u = A -> ( ( f : u --> B /\ A. x e. u ps ) <-> ( f : A --> B /\ A. x e. A ps ) ) )
36	35	exbidv 1818	. . . 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 5388	. . . 4 |- (/) : (/) --> B
39		0ex 4116	. . . . 5 |- (/) e. _V
40		ral0 3516	. . . . . . 7 |- A. x e. (/) ps
41	40	biantru 300	. . . . . 6 |- ( f : (/) --> B <-> ( f : (/) --> B /\ A. x e. (/) ps ) )
42		feq1 5330	. . . . . 6 |- ( f = (/) -> ( f : (/) --> B <-> (/) : (/) --> B ) )
43	41, 42	bitr3id 193	. . . . 5 |- ( f = (/) -> ( ( f : (/) --> B /\ A. x e. (/) ps ) <-> (/) : (/) --> B ) )
44	39, 43	spcev 2825	. . . 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 3290	. . . . . . 7 |- w C_ ( w u. { z } )
47		ssralv 3211	. . . . . . 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 3291	. . . . . . . . 9 |- { z } C_ ( w u. { z } )
51		ssralv 3211	. . . . . . . . 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 2733	. . . . . . . . . 10 |- z e. _V
54		ralsnsg 3620	. . . . . . . . . 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 3034	. . . . . . . . 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 1521	. . . . . . . 8 |- F/ y -. z e. w
60		nfv 1521	. . . . . . . . 9 |- F/ y E. f ( f : w --> B /\ A. x e. w ps )
61		nfv 1521	. . . . . . . . . . 11 |- F/ y g : ( w u. { z } ) --> B
62		nfcv 2312	. . . . . . . . . . . 12 |- F/_ y ( w u. { z } )
63		nfsbc1v 2973	. . . . . . . . . . . 12 |- F/ y [. ( g ` x ) / y ]. ph
64	62, 63	nfralxy 2508	. . . . . . . . . . 11 |- F/ y A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph
65	61, 64	nfan 1558	. . . . . . . . . 10 |- F/ y ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
66	65	nfex 1630	. . . . . . . . 9 |- F/ y E. g ( g : ( w u. { z } ) --> B /\ A. x e. ( w u. { z } ) [. ( g ` x ) / y ]. ph )
67	60, 66	nfim 1565	. . . . . . . 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 526	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> f : w --> B )
69		vex 2733	. . . . . . . . . . . . . . . 16 |- y e. _V
70	53, 69	f1osn 5482	. . . . . . . . . . . . . . 15 |- { <. z , y >. } : { z } -1-1-onto-> { y }
71		f1of 5442	. . . . . . . . . . . . . . 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 996	. . . . . . . . . . . . . . 15 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> y e. B )
74	73	snssd 3725	. . . . . . . . . . . . . 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 5360	. . . . . . . . . . . . 13 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> { <. z , y >. } : { z } --> B )
76		simpl1 995	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> -. z e. w )
77		disjsn 3645	. . . . . . . . . . . . . 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 5371	. . . . . . . . . . . . 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 1232	. . . . . . . . . . . 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 527	. . . . . . . . . . . . . 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 2242	. . . . . . . . . . . . . . . . . . 19 |- ( x e. w -> ( z = x -> z e. w ) )
83	82	necon3bd 2383	. . . . . . . . . . . . . . . . . 18 |- ( x e. w -> ( -. z e. w -> z =/= x ) )
84	83	impcom 124	. . . . . . . . . . . . . . . . 17 |- ( ( -. z e. w /\ x e. w ) -> z =/= x )
85		fvunsng 5690	. . . . . . . . . . . . . . . . . 18 |- ( ( x e. _V /\ z =/= x ) -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
86	20, 85	mpan 422	. . . . . . . . . . . . . . . . 17 |- ( z =/= x -> ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) )
87		dfsbcq 2957	. . . . . . . . . . . . . . . . . 18 |- ( ( ( f u. { <. z , y >. } ) ` x ) = ( f ` x ) -> ( [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph <-> [. ( f ` x ) / y ]. ph ) )
88	87, 23	bitr2di 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 2466	. . . . . . . . . . . . . . 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 997	. . . . . . . . . . . . . 14 |- ( ( ( -. z e. w /\ y e. B /\ [. z / x ]. ph ) /\ ( f : w --> B /\ A. x e. w ps ) ) -> [. z / x ]. ph )
94		ffun 5350	. . . . . . . . . . . . . . . . 17 |- ( ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B -> Fun ( f u. { <. z , y >. } ) )
95		ssun2 3291	. . . . . . . . . . . . . . . . . 18 |- { <. z , y >. } C_ ( f u. { <. z , y >. } )
96		vsnid 3615	. . . . . . . . . . . . . . . . . . 19 |- z e. { z }
97	69	dmsnop 5084	. . . . . . . . . . . . . . . . . . 19 |- dom { <. z , y >. } = { z }
98	96, 97	eleqtrri 2246	. . . . . . . . . . . . . . . . . 18 |- z e. dom { <. z , y >. }
99		funssfv 5522	. . . . . . . . . . . . . . . . . 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 1324	. . . . . . . . . . . . . . . . 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 5691	. . . . . . . . . . . . . . . 16 |- ( { <. z , y >. } ` z ) = y
103	101, 102	eqtr2di 2220	. . . . . . . . . . . . . . 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 3620	. . . . . . . . . . . . . . . . 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 3601	. . . . . . . . . . . . . . . . . . . . 21 |- ( x e. { z } -> x = z )
107	106	fveq2d 5500	. . . . . . . . . . . . . . . . . . . 20 |- ( x e. { z } -> ( ( f u. { <. z , y >. } ) ` x ) = ( ( f u. { <. z , y >. } ) ` z ) )
108	107	eqeq2d 2182	. . . . . . . . . . . . . . . . . . 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 2964	. . . . . . . . . . . . . . . . . 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 2466	. . . . . . . . . . . . . . . 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 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 3309	. . . . . . . . . . . . 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 409	. . . . . . . . . . . 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 4214	. . . . . . . . . . . . . . 15 |- <. z , y >. e. _V
119	118	snex 4171	. . . . . . . . . . . . . 14 |- { <. z , y >. } e. _V
120	19, 119	unex 4426	. . . . . . . . . . . . 13 |- ( f u. { <. z , y >. } ) e. _V
121		feq1 5330	. . . . . . . . . . . . . 14 |- ( g = ( f u. { <. z , y >. } ) -> ( g : ( w u. { z } ) --> B <-> ( f u. { <. z , y >. } ) : ( w u. { z } ) --> B ) )
122		fveq1 5495	. . . . . . . . . . . . . . . 16 |- ( g = ( f u. { <. z , y >. } ) -> ( g ` x ) = ( ( f u. { <. z , y >. } ) ` x ) )
123	122	sbceq1d 2960	. . . . . . . . . . . . . . 15 |- ( g = ( f u. { <. z , y >. } ) -> ( [. ( g ` x ) / y ]. ph <-> [. ( ( f u. { <. z , y >. } ) ` x ) / y ]. ph ) )
124	123	ralbidv 2470	. . . . . . . . . . . . . 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 470	. . . . . . . . . . . . 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 2825	. . . . . . . . . . . 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 409	. . . . . . . . . . 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 1812	. . . . . . . . 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 1197	. . . . . . . 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 2584	. . . . . . 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 6868	. 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 973   = wceq 1348   E.wex 1485   e. wcel 2141   =/= wne 2340   A.wral 2448   E.wrex 2449   _Vcvv 2730   [.wsbc 2955   u. cun 3119   i^i cin 3120   C_ wss 3121   (/)c0 3414   {csn 3583   <.cop 3586   dom cdm 4611   Fun wfun 5192   -->wf 5194   -1-1-onto->wf1o 5197   ` cfv 5198   Fincfn 6718

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 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-coll 4104  ax-sep 4107  ax-nul 4115  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-iinf 4572

This theorem depends on definitions:  df-bi 116  df-dc 830  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-ral 2453  df-rex 2454  df-reu 2455  df-rab 2457  df-v 2732  df-sbc 2956  df-csb 3050  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-nul 3415  df-if 3527  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-iun 3875  df-br 3990  df-opab 4051  df-mpt 4052  df-tr 4088  df-id 4278  df-iord 4351  df-on 4353  df-suc 4356  df-iom 4575  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-rn 4622  df-res 4623  df-ima 4624  df-iota 5160  df-fun 5200  df-fn 5201  df-f 5202  df-f1 5203  df-fo 5204  df-f1o 5205  df-fv 5206  df-er 6513  df-en 6719  df-fin 6721

This theorem is referenced by: (None)