Theorem 2ndconst 4097

Description: The mapping of a restriction of the 2nd function to a converse constant function.

Assertion

Ref	Expression
2ndconst	|- (A e. C -> (2nd |` ({A} X. B)):({A} X. B)-1-1-onto->B)

Proof of Theorem 2ndconst

Step	Hyp	Ref	Expression
1		fveq2 3724	. . . . . . . . . . . . . . . . . . 19 |- (x = <.A, w>. -> (2nd` x) = (2nd` <.A, w>.))
2		visset 1813	. . . . . . . . . . . . . . . . . . . 20 |- w e. V
3		op2ndg 4088	. . . . . . . . . . . . . . . . . . . 20 |- ((A e. C /\ w e. V) -> (2nd` <.A, w>.) = w)
4	2, 3	mpan2 696	. . . . . . . . . . . . . . . . . . 19 |- (A e. C -> (2nd` <.A, w>.) = w)
5	1, 4	sylan9eqr 1529	. . . . . . . . . . . . . . . . . 18 |- ((A e. C /\ x = <.A, w>.) -> (2nd` x) = w)
6	5	eqeq1d 1483	. . . . . . . . . . . . . . . . 17 |- ((A e. C /\ x = <.A, w>.) -> ((2nd` x) = y <-> w = y))
7	6	anbi1d 617	. . . . . . . . . . . . . . . 16 |- ((A e. C /\ x = <.A, w>.) -> (((2nd` x) = y /\ w e. B) <-> (w = y /\ w e. B)))
8	7	pm5.32da 649	. . . . . . . . . . . . . . 15 |- (A e. C -> ((x = <.A, w>. /\ ((2nd` x) = y /\ w e. B)) <-> (x = <.A, w>. /\ (w = y /\ w e. B))))
9		an12 484	. . . . . . . . . . . . . . 15 |- (((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> (x = <.A, w>. /\ ((2nd` x) = y /\ w e. B)))
10		an12 484	. . . . . . . . . . . . . . 15 |- ((w = y /\ (x = <.A, w>. /\ w e. B)) <-> (x = <.A, w>. /\ (w = y /\ w e. B)))
11	8, 9, 10	3bitr4g 555	. . . . . . . . . . . . . 14 |- (A e. C -> (((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> (w = y /\ (x = <.A, w>. /\ w e. B))))
12	11	exbidv 1279	. . . . . . . . . . . . 13 |- (A e. C -> (E.w((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> E.w(w = y /\ (x = <.A, w>. /\ w e. B))))
13		visset 1813	. . . . . . . . . . . . . . 15 |- y e. V
14		opeq2 2488	. . . . . . . . . . . . . . . . 17 |- (w = y -> <.A, w>. = <.A, y>.)
15	14	eqeq2d 1486	. . . . . . . . . . . . . . . 16 |- (w = y -> (x = <.A, w>. <-> x = <.A, y>.))
16		eleq1 1534	. . . . . . . . . . . . . . . 16 |- (w = y -> (w e. B <-> y e. B))
17	15, 16	anbi12d 628	. . . . . . . . . . . . . . 15 |- (w = y -> ((x = <.A, w>. /\ w e. B) <-> (x = <.A, y>. /\ y e. B)))
18	13, 17	ceqsexv 1835	. . . . . . . . . . . . . 14 |- (E.w(w = y /\ (x = <.A, w>. /\ w e. B)) <-> (x = <.A, y>. /\ y e. B))
19		ancom 435	. . . . . . . . . . . . . 14 |- ((x = <.A, y>. /\ y e. B) <-> (y e. B /\ x = <.A, y>.))
20	18, 19	bitr 173	. . . . . . . . . . . . 13 |- (E.w(w = y /\ (x = <.A, w>. /\ w e. B)) <-> (y e. B /\ x = <.A, y>.))
21	12, 20	syl6rbb 537	. . . . . . . . . . . 12 |- (A e. C -> ((y e. B /\ x = <.A, y>.) <-> E.w((2nd` x) = y /\ (x = <.A, w>. /\ w e. B))))
22		opeq1 2487	. . . . . . . . . . . . . . . . . . . . 21 |- (z = A -> <.z, w>. = <.A, w>.)
23	22	eqeq2d 1486	. . . . . . . . . . . . . . . . . . . 20 |- (z = A -> (x = <.z, w>. <-> x = <.A, w>.))
24	23	anbi1d 617	. . . . . . . . . . . . . . . . . . 19 |- (z = A -> ((x = <.z, w>. /\ w e. B) <-> (x = <.A, w>. /\ w e. B)))
25	24	ceqsexgv 1888	. . . . . . . . . . . . . . . . . 18 |- (A e. C -> (E.z(z = A /\ (x = <.z, w>. /\ w e. B)) <-> (x = <.A, w>. /\ w e. B)))
26		elsn 2421	. . . . . . . . . . . . . . . . . . . . . 22 |- (z e. {A} <-> z = A)
27	26	anbi1i 481	. . . . . . . . . . . . . . . . . . . . 21 |- ((z e. {A} /\ w e. B) <-> (z = A /\ w e. B))
28	27	anbi2i 480	. . . . . . . . . . . . . . . . . . . 20 |- ((x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> (x = <.z, w>. /\ (z = A /\ w e. B)))
29		an12 484	. . . . . . . . . . . . . . . . . . . 20 |- ((x = <.z, w>. /\ (z = A /\ w e. B)) <-> (z = A /\ (x = <.z, w>. /\ w e. B)))
30	28, 29	bitr 173	. . . . . . . . . . . . . . . . . . 19 |- ((x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> (z = A /\ (x = <.z, w>. /\ w e. B)))
31	30	exbii 1051	. . . . . . . . . . . . . . . . . 18 |- (E.z(x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> E.z(z = A /\ (x = <.z, w>. /\ w e. B)))
32	25, 31	syl5bb 532	. . . . . . . . . . . . . . . . 17 |- (A e. C -> (E.z(x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> (x = <.A, w>. /\ w e. B)))
33	32	exbidv 1279	. . . . . . . . . . . . . . . 16 |- (A e. C -> (E.wE.z(x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> E.w(x = <.A, w>. /\ w e. B)))
34		excom 1046	. . . . . . . . . . . . . . . 16 |- (E.zE.w(x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> E.wE.z(x = <.z, w>. /\ (z e. {A} /\ w e. B)))
35	33, 34	syl5bb 532	. . . . . . . . . . . . . . 15 |- (A e. C -> (E.zE.w(x = <.z, w>. /\ (z e. {A} /\ w e. B)) <-> E.w(x = <.A, w>. /\ w e. B)))
36		elxp 3202	. . . . . . . . . . . . . . 15 |- (x e. ({A} X. B) <-> E.zE.w(x = <.z, w>. /\ (z e. {A} /\ w e. B)))
37	35, 36	syl5rbb 533	. . . . . . . . . . . . . 14 |- (A e. C -> (E.w(x = <.A, w>. /\ w e. B) <-> x e. ({A} X. B)))
38	37	anbi2d 616	. . . . . . . . . . . . 13 |- (A e. C -> ((x2ndy /\ E.w(x = <.A, w>. /\ w e. B)) <-> (x2ndy /\ x e. ({A} X. B))))
39		19.42v 1308	. . . . . . . . . . . . . 14 |- (E.w((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> ((2nd` x) = y /\ E.w(x = <.A, w>. /\ w e. B)))
40		fo2nd 4092	. . . . . . . . . . . . . . . . . 18 |- 2nd:V-onto->V
41		fof 3672	. . . . . . . . . . . . . . . . . 18 |- (2nd:V-onto->V -> 2nd:V-->V)
42	40, 41	ax-mp 7	. . . . . . . . . . . . . . . . 17 |- 2nd:V-->V
43		ffn 3627	. . . . . . . . . . . . . . . . 17 |- (2nd:V-->V -> 2nd Fn V)
44	42, 43	ax-mp 7	. . . . . . . . . . . . . . . 16 |- 2nd Fn V
45		visset 1813	. . . . . . . . . . . . . . . 16 |- x e. V
46	13	fnbrfvb 3753	. . . . . . . . . . . . . . . 16 |- ((2nd Fn V /\ x e. V) -> ((2nd` x) = y <-> x2ndy))
47	44, 45, 46	mp2an 697	. . . . . . . . . . . . . . 15 |- ((2nd` x) = y <-> x2ndy)
48	47	anbi1i 481	. . . . . . . . . . . . . 14 |- (((2nd` x) = y /\ E.w(x = <.A, w>. /\ w e. B)) <-> (x2ndy /\ E.w(x = <.A, w>. /\ w e. B)))
49	39, 48	bitr 173	. . . . . . . . . . . . 13 |- (E.w((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> (x2ndy /\ E.w(x = <.A, w>. /\ w e. B)))
50	38, 49	syl5bb 532	. . . . . . . . . . . 12 |- (A e. C -> (E.w((2nd` x) = y /\ (x = <.A, w>. /\ w e. B)) <-> (x2ndy /\ x e. ({A} X. B))))
51	21, 50	bitr2d 529	. . . . . . . . . . 11 |- (A e. C -> ((x2ndy /\ x e. ({A} X. B)) <-> (y e. B /\ x = <.A, y>.)))
52		ancom 435	. . . . . . . . . . 11 |- ((x e. ({A} X. B) /\ x2ndy) <-> (x2ndy /\ x e. ({A} X. B)))
53	51, 52	syl5bb 532	. . . . . . . . . 10 |- (A e. C -> ((x e. ({A} X. B) /\ x2ndy) <-> (y e. B /\ x = <.A, y>.)))
54	53	exbidv 1279	. . . . . . . . 9 |- (A e. C -> (E.x(x e. ({A} X. B) /\ x2ndy) <-> E.x(y e. B /\ x = <.A, y>.)))
55		19.42v 1308	. . . . . . . . . 10 |- (E.x(y e. B /\ x = <.A, y>.) <-> (y e. B /\ E.x x = <.A, y>.))
56		opex 2782	. . . . . . . . . . 11 |- <.A, y>. e. V
57	56	isseti 1815	. . . . . . . . . 10 |- E.x x = <.A, y>.
58	55, 57	mpbiran2 729	. . . . . . . . 9 |- (E.x(y e. B /\ x = <.A, y>.) <-> y e. B)
59	54, 58	syl6bb 536	. . . . . . . 8 |- (A e. C -> (E.x(x e. ({A} X. B) /\ x2ndy) <-> y e. B))
60	13	elima2 3409	. . . . . . . 8 |- (y e. (2nd"({A} X. B)) <-> E.x(x e. ({A} X. B) /\ x2ndy))
61	59, 60	syl5bb 532	. . . . . . 7 |- (A e. C -> (y e. (2nd"({A} X. B)) <-> y e. B))
62	61	eqrdv