Theorem upxp 10225

Description: Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
upxp.1	|- P = (1st |` (B X. C))
upxp.2	|- Q = (2nd |` (B X. C))

Assertion

Ref	Expression
upxp	|- ((A e. D /\ F:A-->B /\ G:A-->C) -> E!h(h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)))

Distinct variable groups:   A,h   B,h   C,h   D,h   h,F   h,G   P,h   Q,h

Proof of Theorem upxp

Step	Hyp	Ref	Expression
1		opabex2g 4540	. . . 4 |- (A e. D -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} e. _V)
2		eueq 2427	. . . 4 |- ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} e. _V <-> E!h h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
3	1, 2	sylib 215	. . 3 |- (A e. D -> E!h h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
4	3	3ad2ant1 897	. 2 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> E!h h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
5		ffn 4562	. . . . . . . . 9 |- (h:A-->(B X. C) -> h Fn A)
6	5	3ad2ant1 897	. . . . . . . 8 |- ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) -> h Fn A)
7	6	adantl 424	. . . . . . 7 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> h Fn A)
8		opelxpi 4040	. . . . . . . . . . . . . 14 |- (((F` x) e. B /\ (G` x) e. C) -> <.(F` x), (G` x)>. e. (B X. C))
9		ffvelrn 4787	. . . . . . . . . . . . . 14 |- ((F:A-->B /\ x e. A) -> (F` x) e. B)
10		ffvelrn 4787	. . . . . . . . . . . . . 14 |- ((G:A-->C /\ x e. A) -> (G` x) e. C)
11	8, 9, 10	syl2an 503	. . . . . . . . . . . . 13 |- (((F:A-->B /\ x e. A) /\ (G:A-->C /\ x e. A)) -> <.(F` x), (G` x)>. e. (B X. C))
12	11	anandirs 571	. . . . . . . . . . . 12 |- (((F:A-->B /\ G:A-->C) /\ x e. A) -> <.(F` x), (G` x)>. e. (B X. C))
13	12	r19.21aiva 2176	. . . . . . . . . . 11 |- ((F:A-->B /\ G:A-->C) -> A.x e. A <.(F` x), (G` x)>. e. (B X. C))
14	13	3adant1 894	. . . . . . . . . 10 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> A.x e. A <.(F` x), (G` x)>. e. (B X. C))
15		eqid 1884	. . . . . . . . . . 11 |- {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}
16	15	fopab2 4796	. . . . . . . . . 10 |- (A.x e. A <.(F` x), (G` x)>. e. (B X. C) <-> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C))
17	14, 16	sylib 215	. . . . . . . . 9 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C))
18		ffn 4562	. . . . . . . . 9 |- ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A)
19	17, 18	syl 12	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A)
20	19	adantr 425	. . . . . . 7 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A)
21		eqfnfv 4766	. . . . . . 7 |- ((h Fn A /\ {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A) -> (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} <-> (A = A /\ A.z e. A (h` z) = ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z))))
22	7, 20, 21	syl11anc 524	. . . . . 6 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} <-> (A = A /\ A.z e. A (h` z) = ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z))))
23		eqidd 1885	. . . . . 6 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> A = A)
24		ffvelrn 4787	. . . . . . . . . . . 12 |- ((h:A-->(B X. C) /\ z e. A) -> (h` z) e. (B X. C))
25		xpss 4056	. . . . . . . . . . . . 13 |- (B X. C) C_ (_V X. _V)
26	25	sseli 2617	. . . . . . . . . . . 12 |- ((h` z) e. (B X. C) -> (h` z) e. (_V X. _V))
27	24, 26	syl 12	. . . . . . . . . . 11 |- ((h:A-->(B X. C) /\ z e. A) -> (h` z) e. (_V X. _V))
28	27	3ad2antl1 1038	. . . . . . . . . 10 |- (((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) /\ z e. A) -> (h` z) e. (_V X. _V))
29	28	adantll 428	. . . . . . . . 9 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (h` z) e. (_V X. _V))
30		fveq1 4680	. . . . . . . . . . . . 13 |- (F = (P o. h) -> (F` z) = ((P o. h)` z))
31		upxp.1	. . . . . . . . . . . . . . 15 |- P = (1st |` (B X. C))
32	31	coeq1i 4125	. . . . . . . . . . . . . 14 |- (P o. h) = ((1st |` (B X. C)) o. h)
33	32	fveq1i 4682	. . . . . . . . . . . . 13 |- ((P o. h)` z) = (((1st |` (B X. C)) o. h)` z)
34	30, 33	syl6eq 1944	. . . . . . . . . . . 12 |- (F = (P o. h) -> (F` z) = (((1st |` (B X. C)) o. h)` z))
35	34	3ad2ant2 898	. . . . . . . . . . 11 |- ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) -> (F` z) = (((1st |` (B X. C)) o. h)` z))
36	35	ad2antlr 441	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (F` z) = (((1st |` (B X. C)) o. h)` z))
37		fo1st 5032	. . . . . . . . . . . . . . 15 |- 1st:_V-onto->_V
38		fofn 4619	. . . . . . . . . . . . . . 15 |- (1st:_V-onto->_V -> 1st Fn _V)
39	37, 38	ax-mp 7	. . . . . . . . . . . . . 14 |- 1st Fn _V
40		ssv 2636	. . . . . . . . . . . . . 14 |- (B X. C) C_ _V
41		fnssres 4526	. . . . . . . . . . . . . 14 |- ((1st Fn _V /\ (B X. C) C_ _V) -> (1st |` (B X. C)) Fn (B X. C))
42	39, 40, 41	mp2an 761	. . . . . . . . . . . . 13 |- (1st |` (B X. C)) Fn (B X. C)
43		fnfun 4510	. . . . . . . . . . . . 13 |- ((1st |` (B X. C)) Fn (B X. C) -> Fun (1st |` (B X. C)))
44	42, 43	ax-mp 7	. . . . . . . . . . . 12 |- Fun (1st |` (B X. C))
45	44	a1i 8	. . . . . . . . . . 11 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> Fun (1st |` (B X. C)))
46		ffun 4565	. . . . . . . . . . . . 13 |- (h:A-->(B X. C) -> Fun h)
47	46	3ad2ant1 897	. . . . . . . . . . . 12 |- ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) -> Fun h)
48	47	ad2antlr 441	. . . . . . . . . . 11 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> Fun h)
49		fdm 4567	. . . . . . . . . . . . . . 15 |- (h:A-->(B X. C) -> dom h = A)
50	49	eleq2d 1964	. . . . . . . . . . . . . 14 |- (h:A-->(B X. C) -> (z e. dom h <-> z e. A))
51	50	biimpar 461	. . . . . . . . . . . . 13 |- ((h:A-->(B X. C) /\ z e. A) -> z e. dom h)
52	51	3ad2antl1 1038	. . . . . . . . . . . 12 |- (((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) /\ z e. A) -> z e. dom h)
53	52	adantll 428	. . . . . . . . . . 11 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> z e. dom h)
54		fvco 4736	. . . . . . . . . . 11 |- ((Fun (1st |` (B X. C)) /\ Fun h /\ z e. dom h) -> (((1st |` (B X. C)) o. h)` z) = ((1st |` (B X. C))` (h` z)))
55	45, 48, 53, 54	syl111anc 1100	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (((1st |` (B X. C)) o. h)` z) = ((1st |` (B X. C))` (h` z)))
56	24	3ad2antl1 1038	. . . . . . . . . . . 12 |- (((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) /\ z e. A) -> (h` z) e. (B X. C))
57	56	adantll 428	. . . . . . . . . . 11 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (h` z) e. (B X. C))
58		fvres 4691	. . . . . . . . . . 11 |- ((h` z) e. (B X. C) -> ((1st |` (B X. C))` (h` z)) = (1st` (h` z)))
59	57, 58	syl 12	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> ((1st |` (B X. C))` (h` z)) = (1st` (h` z)))
60	36, 55, 59	3eqtrrd 1930	. . . . . . . . 9 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (1st` (h` z)) = (F` z))
61		fveq1 4680	. . . . . . . . . . . . 13 |- (G = (Q o. h) -> (G` z) = ((Q o. h)` z))
62		upxp.2	. . . . . . . . . . . . . . 15 |- Q = (2nd |` (B X. C))
63	62	coeq1i 4125	. . . . . . . . . . . . . 14 |- (Q o. h) = ((2nd |` (B X. C)) o. h)
64	63	fveq1i 4682	. . . . . . . . . . . . 13 |- ((Q o. h)` z) = (((2nd |` (B X. C)) o. h)` z)
65	61, 64	syl6eq 1944	. . . . . . . . . . . 12 |- (G = (Q o. h) -> (G` z) = (((2nd |` (B X. C)) o. h)` z))
66	65	3ad2ant3 899	. . . . . . . . . . 11 |- ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) -> (G` z) = (((2nd |` (B X. C)) o. h)` z))
67	66	ad2antlr 441	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (G` z) = (((2nd |` (B X. C)) o. h)` z))
68		fo2nd 5033	. . . . . . . . . . . . . . 15 |- 2nd:_V-onto->_V
69		fofn 4619	. . . . . . . . . . . . . . 15 |- (2nd:_V-onto->_V -> 2nd Fn _V)
70	68, 69	ax-mp 7	. . . . . . . . . . . . . 14 |- 2nd Fn _V
71		fnssres 4526	. . . . . . . . . . . . . 14 |- ((2nd Fn _V /\ (B X. C) C_ _V) -> (2nd |` (B X. C)) Fn (B X. C))
72	70, 40, 71	mp2an 761	. . . . . . . . . . . . 13 |- (2nd |` (B X. C)) Fn (B X. C)
73		fnfun 4510	. . . . . . . . . . . . 13 |- ((2nd |` (B X. C)) Fn (B X. C) -> Fun (2nd |` (B X. C)))
74	72, 73	ax-mp 7	. . . . . . . . . . . 12 |- Fun (2nd |` (B X. C))
75	74	a1i 8	. . . . . . . . . . 11 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> Fun (2nd |` (B X. C)))
76		fvco 4736	. . . . . . . . . . 11 |- ((Fun (2nd |` (B X. C)) /\ Fun h /\ z e. dom h) -> (((2nd |` (B X. C)) o. h)` z) = ((2nd |` (B X. C))` (h` z)))
77	75, 48, 53, 76	syl111anc 1100	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (((2nd |` (B X. C)) o. h)` z) = ((2nd |` (B X. C))` (h` z)))
78		fvres 4691	. . . . . . . . . . 11 |- ((h` z) e. (B X. C) -> ((2nd |` (B X. C))` (h` z)) = (2nd` (h` z)))
79	57, 78	syl 12	. . . . . . . . . 10 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> ((2nd |` (B X. C))` (h` z)) = (2nd` (h` z)))
80	67, 77, 79	3eqtrrd 1930	. . . . . . . . 9 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (2nd` (h` z)) = (G` z))
81		eqopi 5043	. . . . . . . . 9 |- (((h` z) e. (_V X. _V) /\ ((1st` (h` z)) = (F` z) /\ (2nd` (h` z)) = (G` z))) -> (h` z) = <.(F` z), (G` z)>.)
82	29, 60, 80, 81	syl12anc 1098	. . . . . . . 8 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (h` z) = <.(F` z), (G` z)>.)
83		fveq2 4681	. . . . . . . . . . 11 |- (x = z -> (F` x) = (F` z))
84		fveq2 4681	. . . . . . . . . . 11 |- (x = z -> (G` x) = (G` z))
85	83, 84	opeq12d 3166	. . . . . . . . . 10 |- (x = z -> <.(F` x), (G` x)>. = <.(F` z), (G` z)>.)
86		opex 3527	. . . . . . . . . 10 |- <.(F` z), (G` z)>. e. _V
87	85, 15, 86	fvopab4 4743	. . . . . . . . 9 |- (z e. A -> ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z) = <.(F` z), (G` z)>.)
88	87	adantl 424	. . . . . . . 8 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z) = <.(F` z), (G` z)>.)
89	82, 88	eqtr4d 1928	. . . . . . 7 |- ((((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) /\ z e. A) -> (h` z) = ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z))
90	89	r19.21aiva 2176	. . . . . 6 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> A.z e. A (h` z) = ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z))
91	22, 23, 90	mpbir2and 802	. . . . 5 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))) -> h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
92	91	ex 402	. . . 4 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) -> h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
93		feq1 4551	. . . . . 6 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (h:A-->(B X. C) <-> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C)))
94		coeq2 4124	. . . . . . 7 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (P o. h) = (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
95	94	eqeq2d 1895	. . . . . 6 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (F = (P o. h) <-> F = (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})))
96		coeq2 4124	. . . . . . 7 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (Q o. h) = (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
97	96	eqeq2d 1895	. . . . . 6 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (G = (Q o. h) <-> G = (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})))
98	93, 95, 97	3anbi123d 1168	. . . . 5 |- (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) <-> ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) /\ F = (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))))
99		ffn 4562	. . . . . . . . . 10 |- (F:A-->B -> F Fn A)
100	99	3ad2ant2 898	. . . . . . . . 9 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> F Fn A)
101	42	a1i 8	. . . . . . . . . 10 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (1st |` (B X. C)) Fn (B X. C))
102		frn 4569	. . . . . . . . . . 11 |- ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) -> ran {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} C_ (B X. C))
103	17, 102	syl 12	. . . . . . . . . 10 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ran {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} C_ (B X. C))
104		fnco 4521	. . . . . . . . . 10 |- (((1st |` (B X. C)) Fn (B X. C) /\ {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A /\ ran {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} C_ (B X. C)) -> ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A)
105	101, 19, 103, 104	syl111anc 1100	. . . . . . . . 9 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A)
106		eqfnfv 4766	. . . . . . . . 9 |- ((F Fn A /\ ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A) -> (F = ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) <-> (A = A /\ A.z e. A (F` z) = (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))))
107	100, 105, 106	syl11anc 524	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (F = ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) <-> (A = A /\ A.z e. A (F` z) = (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))))
108		eqidd 1885	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> A = A)
109	44	a1i 8	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> Fun (1st |` (B X. C)))
110	17	adantr 425	. . . . . . . . . . . 12 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C))
111		ffun 4565	. . . . . . . . . . . 12 |- ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) -> Fun {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
112	110, 111	syl 12	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> Fun {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
113		fdm 4567	. . . . . . . . . . . . . 14 |- ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) -> dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} = A)
114	17, 113	syl 12	. . . . . . . . . . . . 13 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} = A)
115	114	eleq2d 1964	. . . . . . . . . . . 12 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (z e. dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} <-> z e. A))
116	115	biimpar 461	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> z e. dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
117		fvco 4736	. . . . . . . . . . 11 |- ((Fun (1st |` (B X. C)) /\ Fun {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} /\ z e. dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) -> (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z) = ((1st |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)))
118	109, 112, 116, 117	syl111anc 1100	. . . . . . . . . 10 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z) = ((1st |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)))
119	87	adantl 424	. . . . . . . . . . . 12 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z) = <.(F` z), (G` z)>.)
120	119	fveq2d 4685	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((1st |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)) = ((1st |` (B X. C))` <.(F` z), (G` z)>.))
121		opelxpi 4040	. . . . . . . . . . . . . . 15 |- (((F` z) e. B /\ (G` z) e. C) -> <.(F` z), (G` z)>. e. (B X. C))
122		ffvelrn 4787	. . . . . . . . . . . . . . 15 |- ((F:A-->B /\ z e. A) -> (F` z) e. B)
123		ffvelrn 4787	. . . . . . . . . . . . . . 15 |- ((G:A-->C /\ z e. A) -> (G` z) e. C)
124	121, 122, 123	syl2an 503	. . . . . . . . . . . . . 14 |- (((F:A-->B /\ z e. A) /\ (G:A-->C /\ z e. A)) -> <.(F` z), (G` z)>. e. (B X. C))
125	124	anandirs 571	. . . . . . . . . . . . 13 |- (((F:A-->B /\ G:A-->C) /\ z e. A) -> <.(F` z), (G` z)>. e. (B X. C))
126	125	3adantl1 1032	. . . . . . . . . . . 12 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> <.(F` z), (G` z)>. e. (B X. C))
127		fvres 4691	. . . . . . . . . . . 12 |- (<.(F` z), (G` z)>. e. (B X. C) -> ((1st |` (B X. C))` <.(F` z), (G` z)>.) = (1st` <.(F` z), (G` z)>.))
128	126, 127	syl 12	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((1st |` (B X. C))` <.(F` z), (G` z)>.) = (1st` <.(F` z), (G` z)>.))
129		fvex 4689	. . . . . . . . . . . . 13 |- (F` z) e. _V
130	129	op1st 5026	. . . . . . . . . . . 12 |- (1st` <.(F` z), (G` z)>.) = (F` z)
131	130	a1i 8	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (1st` <.(F` z), (G` z)>.) = (F` z))
132	120, 128, 131	3eqtrd 1929	. . . . . . . . . 10 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((1st |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)) = (F` z))
133	118, 132	eqtr2d 1926	. . . . . . . . 9 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (F` z) = (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))
134	133	r19.21aiva 2176	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> A.z e. A (F` z) = (((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))
135	107, 108, 134	mpbir2and 802	. . . . . . 7 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> F = ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
136	31	coeq1i 4125	. . . . . . 7 |- (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) = ((1st |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
137	135, 136	syl6eqr 1946	. . . . . 6 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> F = (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
138		ffn 4562	. . . . . . . . . 10 |- (G:A-->C -> G Fn A)
139	138	3ad2ant3 899	. . . . . . . . 9 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> G Fn A)
140	72	a1i 8	. . . . . . . . . 10 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (2nd |` (B X. C)) Fn (B X. C))
141		fnco 4521	. . . . . . . . . 10 |- (((2nd |` (B X. C)) Fn (B X. C) /\ {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} Fn A /\ ran {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} C_ (B X. C)) -> ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A)
142	140, 19, 103, 141	syl111anc 1100	. . . . . . . . 9 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A)
143		eqfnfv 4766	. . . . . . . . 9 |- ((G Fn A /\ ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) Fn A) -> (G = ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) <-> (A = A /\ A.z e. A (G` z) = (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))))
144	139, 142, 143	syl11anc 524	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (G = ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) <-> (A = A /\ A.z e. A (G` z) = (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))))
145	74	a1i 8	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> Fun (2nd |` (B X. C)))
146		fvco 4736	. . . . . . . . . . 11 |- ((Fun (2nd |` (B X. C)) /\ Fun {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} /\ z e. dom {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) -> (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z) = ((2nd |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)))
147	145, 112, 116, 146	syl111anc 1100	. . . . . . . . . 10 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z) = ((2nd |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)))
148	119	fveq2d 4685	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((2nd |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)) = ((2nd |` (B X. C))` <.(F` z), (G` z)>.))
149		fvres 4691	. . . . . . . . . . . 12 |- (<.(F` z), (G` z)>. e. (B X. C) -> ((2nd |` (B X. C))` <.(F` z), (G` z)>.) = (2nd` <.(F` z), (G` z)>.))
150	126, 149	syl 12	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((2nd |` (B X. C))` <.(F` z), (G` z)>.) = (2nd` <.(F` z), (G` z)>.))
151		fvex 4689	. . . . . . . . . . . . 13 |- (G` z) e. _V
152	129, 151	op2nd 5027	. . . . . . . . . . . 12 |- (2nd` <.(F` z), (G` z)>.) = (G` z)
153	152	a1i 8	. . . . . . . . . . 11 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (2nd` <.(F` z), (G` z)>.) = (G` z))
154	148, 150, 153	3eqtrd 1929	. . . . . . . . . 10 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> ((2nd |` (B X. C))` ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}` z)) = (G` z))
155	147, 154	eqtr2d 1926	. . . . . . . . 9 |- (((A e. D /\ F:A-->B /\ G:A-->C) /\ z e. A) -> (G` z) = (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))
156	155	r19.21aiva 2176	. . . . . . . 8 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> A.z e. A (G` z) = (((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})` z))
157	144, 108, 156	mpbir2and 802	. . . . . . 7 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> G = ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
158	62	coeq1i 4125	. . . . . . 7 |- (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) = ((2nd |` (B X. C)) o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})
159	157, 158	syl6eqr 1946	. . . . . 6 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> G = (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
160	17, 137, 159	3jca 1050	. . . . 5 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ({<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}:A-->(B X. C) /\ F = (P o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)})))
161	98, 160	syl5cbir 228	. . . 4 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)} -> (h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h))))
162	92, 161	impbid 574	. . 3 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> ((h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) <-> h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
163	162	eubidv 1779	. 2 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> (E!h(h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)) <-> E!h h = {<.x, y>. | (x e. A /\ y = <.(F` x), (G` x)>.)}))
164	4, 163	mpbird 213	1 |- ((A e. D /\ F:A-->B /\ G:A-->C) -> E!h(h:A-->(B X. C) /\ F = (P o. h) /\ G = (Q o. h)))

Syntax hints:   -> wi 3   <-> wb 163   /\ wa 240   /\ w3a 858   = wceq 1298   e. wcel 1300  E!weu 1771  A.wral 2105  _Vcvv 2292   C_ wss 2593  <.cop 3046  {copab 3395   X. cxp 3984  dom cdm 3986  ran crn 3987   |` cres 3988   o. ccom 3990  Fun wfun 3992   Fn wfn 3993  -->wf 3994  -onto->wfo 3996  ` cfv 3998  1stc1st 5018  2ndc2nd 5019

This theorem is referenced by:  uptx 10226  txcn 10227

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1304  ax-gen 1305  ax-8 1306  ax-9 1307  ax-10 1308  ax-11 1309  ax-12 1310  ax-13 1311  ax-14 1312  ax-17 1317  ax-4 1319  ax-5o 1321  ax-6o 1324  ax-9o 1481  ax-10o 1500  ax-16 1580  ax-11o 1588  ax-ext 1865  ax-rep 3428  ax-sep 3438  ax-nul 3445  ax-pow 3481  ax-pr 3524  ax-un 3790

This theorem depends on definitions:  df-bi 164  df-or 241  df-an 242  df-3an 860  df-ex 1327  df-sb 1536  df-eu 1775  df-mo 1776  df-clab 1872  df-cleq 1877  df-clel 1880  df-ne 2019  df-ral 2109  df-rex 2110  df-v 2294  df-dif 2597  df-un 2600  df-in 2603  df-ss 2605  df-nul 2876  df-pw 3035  df-sn 3049  df-pr 3050  df-op 3053  df-uni 3178  df-br 3339  df-opab 3396  df-id 3586  df-xp 4000  df-rel 4001  df-cnv 4002  df-co 4003  df-dm 4004  df-rn 4005  df-res 4006  df-ima 4007  df-fun 4008  df-fn 4009  df-f 4010  df-fo 4012  df-fv 4014  df-1st 5020  df-2nd 5021

Copyright terms: Public domain