Theorem enprmaplem3 6079

Description: Lemma for enprmap 6083. The converse of W is a function. (Contributed by SF, 3-Mar-2015.)

Hypothesis

Ref	Expression
enprmaplem3.1	|- W = (r e. (A ^m B) |-> (`'r"{x}))

Assertion

Ref	Expression
enprmaplem3	|- ((x =/= y /\ A = {x, y}) -> Fun `'W)

Distinct variable groups:   A,r   B,r   x,r

Allowed substitution hints:   A(x,y)   B(x,y)   W(x,y,r)

Proof of Theorem enprmaplem3

Dummy variables p q w z are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		brcnv 4893	. . . . . 6 |- (z`'Wp <-> pWz)
2		brcnv 4893	. . . . . 6 |- (z`'Wq <-> qWz)
3		breldm 4912	. . . . . . . . 9 |- (pWz -> p e. dom W)
4		enprmaplem3.1	. . . . . . . . . . 11 |- W = (r e. (A ^m B) |-> (`'r"{x}))
5	4	enprmaplem2 6078	. . . . . . . . . 10 |- W Fn (A ^m B)
6		fndm 5183	. . . . . . . . . 10 |- (W Fn (A ^m B) -> dom W = (A ^m B))
7	5, 6	ax-mp 5	. . . . . . . . 9 |- dom W = (A ^m B)
8	3, 7	syl6eleq 2443	. . . . . . . 8 |- (pWz -> p e. (A ^m B))
9		fnfun 5182	. . . . . . . . . . 11 |- (W Fn (A ^m B) -> Fun W)
10	5, 9	ax-mp 5	. . . . . . . . . 10 |- Fun W
11		funbrfv 5357	. . . . . . . . . 10 |- (Fun W -> (pWz -> (W` p) = z))
12	10, 11	ax-mp 5	. . . . . . . . 9 |- (pWz -> (W` p) = z)
13		cnveq 4887	. . . . . . . . . . . 12 |- (r = p -> `'r = `'p)
14	13	imaeq1d 4942	. . . . . . . . . . 11 |- (r = p -> (`'r"{x}) = (`'p"{x}))
15		vex 2863	. . . . . . . . . . . . 13 |- p e. _V
16	15	cnvex 5103	. . . . . . . . . . . 12 |- `'p e. _V
17		snex 4112	. . . . . . . . . . . 12 |- {x} e. _V
18	16, 17	imaex 4748	. . . . . . . . . . 11 |- (`'p"{x}) e. _V
19	14, 4, 18	fvmpt 5701	. . . . . . . . . 10 |- (p e. (A ^m B) -> (W` p) = (`'p"{x}))
20	8, 19	syl 15	. . . . . . . . 9 |- (pWz -> (W` p) = (`'p"{x}))
21	12, 20	eqtr3d 2387	. . . . . . . 8 |- (pWz -> z = (`'p"{x}))
22	8, 21	jca 518	. . . . . . 7 |- (pWz -> (p e. (A ^m B) /\ z = (`'p"{x})))
23		breldm 4912	. . . . . . . . 9 |- (qWz -> q e. dom W)
24	23, 7	syl6eleq 2443	. . . . . . . 8 |- (qWz -> q e. (A ^m B))
25		funbrfv 5357	. . . . . . . . . 10 |- (Fun W -> (qWz -> (W` q) = z))
26	10, 25	ax-mp 5	. . . . . . . . 9 |- (qWz -> (W` q) = z)
27		cnveq 4887	. . . . . . . . . . . 12 |- (r = q -> `'r = `'q)
28	27	imaeq1d 4942	. . . . . . . . . . 11 |- (r = q -> (`'r"{x}) = (`'q"{x}))
29		vex 2863	. . . . . . . . . . . . 13 |- q e. _V
30	29	cnvex 5103	. . . . . . . . . . . 12 |- `'q e. _V
31	30, 17	imaex 4748	. . . . . . . . . . 11 |- (`'q"{x}) e. _V
32	28, 4, 31	fvmpt 5701	. . . . . . . . . 10 |- (q e. (A ^m B) -> (W` q) = (`'q"{x}))
33	24, 32	syl 15	. . . . . . . . 9 |- (qWz -> (W` q) = (`'q"{x}))
34	26, 33	eqtr3d 2387	. . . . . . . 8 |- (qWz -> z = (`'q"{x}))
35	24, 34	jca 518	. . . . . . 7 |- (qWz -> (q e. (A ^m B) /\ z = (`'q"{x})))
36	22, 35	anim12i 549	. . . . . 6 |- ((pWz /\ qWz) -> ((p e. (A ^m B) /\ z = (`'p"{x})) /\ (q e. (A ^m B) /\ z = (`'q"{x}))))
37	1, 2, 36	syl2anb 465	. . . . 5 |- ((z`'Wp /\ z`'Wq) -> ((p e. (A ^m B) /\ z = (`'p"{x})) /\ (q e. (A ^m B) /\ z = (`'q"{x}))))
38		elmapi 6017	. . . . . . . . 9 |- (p e. (A ^m B) -> p:B-->A)
39		elmapi 6017	. . . . . . . . 9 |- (q e. (A ^m B) -> q:B-->A)
40	38, 39	anim12i 549	. . . . . . . 8 |- ((p e. (A ^m B) /\ q e. (A ^m B)) -> (p:B-->A /\ q:B-->A))
41		eqtr2 2371	. . . . . . . 8 |- ((z = (`'p"{x}) /\ z = (`'q"{x})) -> (`'p"{x}) = (`'q"{x}))
42		simprll 738	. . . . . . . . . . 11 |- (((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) -> p:B-->A)
43		ffn 5224	. . . . . . . . . . 11 |- (p:B-->A -> p Fn B)
44	42, 43	syl 15	. . . . . . . . . 10 |- (((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) -> p Fn B)
45		simprlr 739	. . . . . . . . . . 11 |- (((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) -> q:B-->A)
46		ffn 5224	. . . . . . . . . . 11 |- (q:B-->A -> q Fn B)
47	45, 46	syl 15	. . . . . . . . . 10 |- (((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) -> q Fn B)
48		ffvelrn 5416	. . . . . . . . . . . 12 |- ((p:B-->A /\ z e. B) -> (p` z) e. A)
49	42, 48	sylan 457	. . . . . . . . . . 11 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (p` z) e. A)
50		simpllr 735	. . . . . . . . . . . . . 14 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> A = {x, y})
51	50	eleq2d 2420	. . . . . . . . . . . . 13 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) e. A <-> (p` z) e. {x, y}))
52		fvex 5340	. . . . . . . . . . . . . 14 |- (p` z) e. _V
53	52	elpr 3752	. . . . . . . . . . . . 13 |- ((p` z) e. {x, y} <-> ((p` z) = x \/ (p` z) = y))
54	51, 53	syl6bb 252	. . . . . . . . . . . 12 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) e. A <-> ((p` z) = x \/ (p` z) = y)))
55		simprr 733	. . . . . . . . . . . . . . 15 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = x)) -> (p` z) = x)
56		simplrr 737	. . . . . . . . . . . . . . . . . . . 20 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (`'p"{x}) = (`'q"{x}))
57	56	eleq2d 2420	. . . . . . . . . . . . . . . . . . 19 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (z e. (`'p"{x}) <-> z e. (`'q"{x})))
58		eliniseg 5021	. . . . . . . . . . . . . . . . . . 19 |- (z e. (`'p"{x}) <-> zpx)
59		eliniseg 5021	. . . . . . . . . . . . . . . . . . 19 |- (z e. (`'q"{x}) <-> zqx)
60	57, 58, 59	3bitr3g 278	. . . . . . . . . . . . . . . . . 18 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpx <-> zqx))
61	60	biimpd 198	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpx -> zqx))
62		fnbrfvb 5359	. . . . . . . . . . . . . . . . . 18 |- ((p Fn B /\ z e. B) -> ((p` z) = x <-> zpx))
63	44, 62	sylan 457	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = x <-> zpx))
64		fnbrfvb 5359	. . . . . . . . . . . . . . . . . 18 |- ((q Fn B /\ z e. B) -> ((q` z) = x <-> zqx))
65	47, 64	sylan 457	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((q` z) = x <-> zqx))
66	61, 63, 65	3imtr4d 259	. . . . . . . . . . . . . . . 16 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = x -> (q` z) = x))
67	66	impr 602	. . . . . . . . . . . . . . 15 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = x)) -> (q` z) = x)
68	55, 67	eqtr4d 2388	. . . . . . . . . . . . . 14 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = x)) -> (p` z) = (q` z))
69	68	expr 598	. . . . . . . . . . . . 13 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = x -> (p` z) = (q` z)))
70		simprr 733	. . . . . . . . . . . . . . 15 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = y)) -> (p` z) = y)
71		simplll 734	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> x =/= y)
72	71	neneqd 2533	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> -. x = y)
73	42	adantr 451	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> p:B-->A)
74		ffun 5226	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (p:B-->A -> Fun p)
75		fununiq 5518	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ((Fun p /\ zpx /\ zpy) -> x = y)
76	75	3expib 1154	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (Fun p -> ((zpx /\ zpy) -> x = y))
77	76	ancomsd 440	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (Fun p -> ((zpy /\ zpx) -> x = y))
78	73, 74, 77	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((zpy /\ zpx) -> x = y))
79	78	exp3a 425	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpy -> (zpx -> x = y)))
80	79	impr 602	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (zpx -> x = y))
81	72, 80	mtod 168	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> -. zpx)
82	81	expr 598	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpy -> -. zpx))
83	60	biimprd 214	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zqx -> zpx))
84	82, 83	nsyld 132	. . . . . . . . . . . . . . . . . . . 20 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpy -> -. zqx))
85	84	impr 602	. . . . . . . . . . . . . . . . . . 19 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> -. zqx)
86		simprl 732	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> z e. B)
87	45	adantr 451	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> q:B-->A)
88		fdm 5227	. . . . . . . . . . . . . . . . . . . . . 22 |- (q:B-->A -> dom q = B)
89	87, 88	syl 15	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> dom q = B)
90	86, 89	eleqtrrd 2430	. . . . . . . . . . . . . . . . . . . 20 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> z e. dom q)
91		eldm 4899	. . . . . . . . . . . . . . . . . . . . 21 |- (z e. dom q <-> E.w zqw)
92		brelrn 4961	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (zqw -> w e. ran q)
93		frn 5229	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (q:B-->A -> ran q C_ A)
94	87, 93	syl 15	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> ran q C_ A)
95	94	sseld 3273	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (w e. ran q -> w e. A))
96	92, 95	syl5 28	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (zqw -> w e. A))
97		simpllr 735	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> A = {x, y})
98	97	eleq2d 2420	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (w e. A <-> w e. {x, y}))
99		vex 2863	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- w e. _V
100	99	elpr 3752	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (w e. {x, y} <-> (w = x \/ w = y))
101		breq2 4644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = x -> (zqw <-> zqx))
102	101	biimpcd 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (zqw -> (w = x -> zqx))
103		breq2 4644	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (w = y -> (zqw <-> zqy))
104	103	biimpcd 215	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (zqw -> (w = y -> zqy))
105	102, 104	orim12d 811	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (zqw -> ((w = x \/ w = y) -> (zqx \/ zqy)))
106	105	com12 27	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ((w = x \/ w = y) -> (zqw -> (zqx \/ zqy)))
107	100, 106	sylbi 187	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (w e. {x, y} -> (zqw -> (zqx \/ zqy)))
108	98, 107	syl6bi 219	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (w e. A -> (zqw -> (zqx \/ zqy))))
109	108	com23 72	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (zqw -> (w e. A -> (zqx \/ zqy))))
110	96, 109	mpdd 36	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (zqw -> (zqx \/ zqy)))
111	110	exlimdv 1636	. . . . . . . . . . . . . . . . . . . . 21 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (E.w zqw -> (zqx \/ zqy)))
112	91, 111	syl5bi 208	. . . . . . . . . . . . . . . . . . . 20 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (z e. dom q -> (zqx \/ zqy)))
113	90, 112	mpd 14	. . . . . . . . . . . . . . . . . . 19 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> (zqx \/ zqy))
114		orel1 371	. . . . . . . . . . . . . . . . . . 19 |- (-. zqx -> ((zqx \/ zqy) -> zqy))
115	85, 113, 114	sylc 56	. . . . . . . . . . . . . . . . . 18 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ zpy)) -> zqy)
116	115	expr 598	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (zpy -> zqy))
117		fnbrfvb 5359	. . . . . . . . . . . . . . . . . 18 |- ((p Fn B /\ z e. B) -> ((p` z) = y <-> zpy))
118	44, 117	sylan 457	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = y <-> zpy))
119		fnbrfvb 5359	. . . . . . . . . . . . . . . . . 18 |- ((q Fn B /\ z e. B) -> ((q` z) = y <-> zqy))
120	47, 119	sylan 457	. . . . . . . . . . . . . . . . 17 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((q` z) = y <-> zqy))
121	116, 118, 120	3imtr4d 259	. . . . . . . . . . . . . . . 16 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = y -> (q` z) = y))
122	121	impr 602	. . . . . . . . . . . . . . 15 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = y)) -> (q` z) = y)
123	70, 122	eqtr4d 2388	. . . . . . . . . . . . . 14 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ (z e. B /\ (p` z) = y)) -> (p` z) = (q` z))
124	123	expr 598	. . . . . . . . . . . . 13 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) = y -> (p` z) = (q` z)))
125	69, 124	jaod 369	. . . . . . . . . . . 12 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (((p` z) = x \/ (p` z) = y) -> (p` z) = (q` z)))
126	54, 125	sylbid 206	. . . . . . . . . . 11 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> ((p` z) e. A -> (p` z) = (q` z)))
127	49, 126	mpd 14	. . . . . . . . . 10 |- ((((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) /\ z e. B) -> (p` z) = (q` z))
128	44, 47, 127	eqfnfvd 5396	. . . . . . . . 9 |- (((x =/= y /\ A = {x, y}) /\ ((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x}))) -> p = q)
129	128	expcom 424	. . . . . . . 8 |- (((p:B-->A /\ q:B-->A) /\ (`'p"{x}) = (`'q"{x})) -> ((x =/= y /\ A = {x, y}) -> p = q))
130	40, 41, 129	syl2an 463	. . . . . . 7 |- (((p e. (A ^m B) /\ q e. (A ^m B)) /\ (z = (`'p"{x}) /\ z = (`'q"{x}))) -> ((x =/= y /\ A = {x, y}) -> p = q))
131	130	an4s 799	. . . . . 6 |- (((p e. (A ^m B) /\ z = (`'p"{x})) /\ (q e. (A ^m B) /\ z = (`'q"{x}))) -> ((x =/= y /\ A = {x, y}) -> p = q))
132	131	com12 27	. . . . 5 |- ((x =/= y /\ A = {x, y}) -> (((p e. (A ^m B) /\ z = (`'p"{x})) /\ (q e. (A ^m B) /\ z = (`'q"{x}))) -> p = q))
133	37, 132	syl5 28	. . . 4 |- ((x =/= y /\ A = {x, y}) -> ((z`'Wp /\ z`'Wq) -> p = q))
134	133	alrimiv 1631	. . 3 |- ((x =/= y /\ A = {x, y}) -> A.q((z`'Wp /\ z`'Wq) -> p = q))
135	134	alrimivv 1632	. 2 |- ((x =/= y /\ A = {x, y}) -> A.zA.pA.q((z`'Wp /\ z`'Wq) -> p = q))
136		dffun2 5120	. 2 |- (Fun `'W <-> A.zA.pA.q((z`'Wp /\ z`'Wq) -> p = q))
137	135, 136	sylibr 203	1 |- ((x =/= y /\ A = {x, y}) -> Fun `'W)

Syntax hints:  -. wn 3   -> wi 4   <-> wb 176   \/ wo 357   /\ wa 358  A.wal 1540  E.wex 1541   = wceq 1642   e. wcel 1710   =/= wne 2517   C_ wss 3258  {csn 3738  {cpr 3739   class class class wbr 4640  "cima 4723  `'ccnv 4772  dom cdm 4773  ran crn 4774  Fun wfun 4776   Fn wfn 4777  -->wf 4778  ` cfv 4782  (class class class)co 5526   |-> cmpt 5652   ^m cmap 6000

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-13 1712  ax-14 1714  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1925  ax-ext 2334  ax-nin 4079  ax-xp 4080  ax-cnv 4081  ax-1c 4082  ax-sset 4083  ax-si 4084  ax-ins2 4085  ax-ins3 4086  ax-typlower 4087  ax-sn 4088

This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3or 935  df-3an 936  df-nan 1288  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-eu 2208  df-mo 2209  df-clab 2340  df-cleq 2346  df-clel 2349  df-nfc 2479  df-ne 2519  df-ral 2620  df-rex 2621  df-reu 2622  df-rmo 2623  df-rab 2624  df-v 2862  df-sbc 3048  df-nin 3212  df-compl 3213  df-in 3214  df-un 3215  df-dif 3216  df-symdif 3217  df-ss 3260  df-pss 3262  df-nul 3552  df-if 3664  df-pw 3725  df-sn 3742  df-pr 3743  df-uni 3893  df-int 3928  df-opk 4059  df-1c 4137  df-pw1 4138  df-uni1 4139  df-xpk 4186  df-cnvk 4187  df-ins2k 4188  df-ins3k 4189  df-imak 4190  df-cok 4191  df-p6 4192  df-sik 4193  df-ssetk 4194  df-imagek 4195  df-idk 4196  df-iota 4340  df-0c 4378  df-addc 4379  df-nnc 4380  df-fin 4381  df-lefin 4441  df-ltfin 4442  df-ncfin 4443  df-tfin 4444  df-evenfin 4445  df-oddfin 4446  df-sfin 4447  df-spfin 4448  df-phi 4566  df-op 4567  df-proj1 4568  df-proj2 4569  df-opab 4624  df-br 4641  df-1st 4724  df-swap 4725  df-sset 4726  df-co 4727  df-ima 4728  df-si 4729  df-id 4768  df-xp 4785  df-cnv 4786  df-rn 4787  df-dm 4788  df-res 4789  df-fun 4790  df-fn 4791  df-f 4792  df-fv 4796  df-2nd 4798  df-ov 5527  df-oprab 5529  df-mpt 5653  df-mpt2 5655  df-txp 5737  df-ins2 5751  df-ins3 5753  df-image 5755  df-ins4 5757  df-si3 5759  df-funs 5761  df-map 6002

This theorem is referenced by:  enprmap  6083