Theorem uptx 11061

Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.)

Hypotheses

Ref	Expression
uptx.1	|- T = (R X.t S)
uptx.2	|- X = U.R
uptx.3	|- Y = U.S
uptx.4	|- Z = (X X. Y)
uptx.5	|- P = (1st |` Z)
uptx.6	|- Q = (2nd |` Z)

Assertion

Ref	Expression
uptx	|- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> E!h e. (U Cn T)(F = (P o. h) /\ G = (Q o. h)))

Distinct variable groups:   R,h   S,h   h,X   T,h   U,h   h,Y   P,h   Q,h   h,Z   h,F   h,G

Proof of Theorem uptx

Step	Hyp	Ref	Expression
1		uniexg 3934	. . . . . 6 |- (U e. Top -> U.U e. _V)
2		opabex2g 4637	. . . . . 6 |- (U.U e. _V -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. _V)
3	1, 2	syl 13	. . . . 5 |- (U e. Top -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. _V)
4	3	3ad2ant3 1143	. . . 4 |- ((R e. Top /\ S e. Top /\ U e. Top) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. _V)
5	4	adantr 447	. . 3 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. _V)
6		uptx.1	. . . . . . . . . 10 |- T = (R X.t S)
7	6	txtop 9792	. . . . . . . . 9 |- ((R e. Top /\ S e. Top) -> T e. Top)
8		eqid 2141	. . . . . . . . . 10 |- U.U = U.U
9		eqid 2141	. . . . . . . . . 10 |- U.T = U.T
10	8, 9	iscn 9900	. . . . . . . . 9 |- ((U e. Top /\ T e. Top) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T /\ A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)))
11	7, 10	sylan2 600	. . . . . . . 8 |- ((U e. Top /\ (R e. Top /\ S e. Top)) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T /\ A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)))
12	11	ancoms 416	. . . . . . 7 |- (((R e. Top /\ S e. Top) /\ U e. Top) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T /\ A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)))
13	12	3impa 1312	. . . . . 6 |- ((R e. Top /\ S e. Top /\ U e. Top) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T /\ A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)))
14	13	adantr 447	. . . . 5 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T /\ A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)))
15		uptx.2	. . . . . . . . . . . . 13 |- X = U.R
16	8, 15	cnf 9904	. . . . . . . . . . . 12 |- ((U e. Top /\ R e. Top /\ F e. (U Cn R)) -> F:U.U-->X)
17	16	3expia 1319	. . . . . . . . . . 11 |- ((U e. Top /\ R e. Top) -> (F e. (U Cn R) -> F:U.U-->X))
18	17	ancoms 416	. . . . . . . . . 10 |- ((R e. Top /\ U e. Top) -> (F e. (U Cn R) -> F:U.U-->X))
19	18	3adant2 1139	. . . . . . . . 9 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (F e. (U Cn R) -> F:U.U-->X))
20		uptx.3	. . . . . . . . . . . . 13 |- Y = U.S
21	8, 20	cnf 9904	. . . . . . . . . . . 12 |- ((U e. Top /\ S e. Top /\ G e. (U Cn S)) -> G:U.U-->Y)
22	21	3expia 1319	. . . . . . . . . . 11 |- ((U e. Top /\ S e. Top) -> (G e. (U Cn S) -> G:U.U-->Y))
23	22	ancoms 416	. . . . . . . . . 10 |- ((S e. Top /\ U e. Top) -> (G e. (U Cn S) -> G:U.U-->Y))
24	23	3adant1 1138	. . . . . . . . 9 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (G e. (U Cn S) -> G:U.U-->Y))
25	19, 24	anim12d 533	. . . . . . . 8 |- ((R e. Top /\ S e. Top /\ U e. Top) -> ((F e. (U Cn R) /\ G e. (U Cn S)) -> (F:U.U-->X /\ G:U.U-->Y)))
26	25	imp 393	. . . . . . 7 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> (F:U.U-->X /\ G:U.U-->Y))
27		ffvelrn 4877	. . . . . . . . . . 11 |- ((F:U.U-->X /\ x e. U.U) -> (F` x) e. X)
28		ffvelrn 4877	. . . . . . . . . . 11 |- ((G:U.U-->Y /\ x e. U.U) -> (G` x) e. Y)
29		opelxpi 4173	. . . . . . . . . . 11 |- (((F` x) e. X /\ (G` x) e. Y) -> <.(F` x), (G` x)>. e. (X X. Y))
30	27, 28, 29	syl2an 603	. . . . . . . . . 10 |- (((F:U.U-->X /\ x e. U.U) /\ (G:U.U-->Y /\ x e. U.U)) -> <.(F` x), (G` x)>. e. (X X. Y))
31	30	anandirs 890	. . . . . . . . 9 |- (((F:U.U-->X /\ G:U.U-->Y) /\ x e. U.U) -> <.(F` x), (G` x)>. e. (X X. Y))
32	31	r19.21aiva 2426	. . . . . . . 8 |- ((F:U.U-->X /\ G:U.U-->Y) -> A.x e. U.U<.(F` x), (G` x)>. e. (X X. Y))
33		eqid 2141	. . . . . . . . 9 |- {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}
34	33	fopab2 4888	. . . . . . . 8 |- (A.x e. U.U<.(F` x), (G` x)>. e. (X X. Y) <-> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y))
35	32, 34	sylib 242	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y))
36	26, 35	syl 13	. . . . . 6 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y))
37	6, 15, 20	txuni 9794	. . . . . . . . 9 |- ((R e. Top /\ S e. Top) -> U.T = (X X. Y))
38	37	3adant3 1140	. . . . . . . 8 |- ((R e. Top /\ S e. Top /\ U e. Top) -> U.T = (X X. Y))
39	38	adantr 447	. . . . . . 7 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> U.T = (X X. Y))
40		feq3 4649	. . . . . . 7 |- (U.T = (X X. Y) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T <-> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y)))
41	39, 40	syl 13	. . . . . 6 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T <-> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y)))
42	36, 41	mpbird 318	. . . . 5 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->U.T)
43		txval 9790	. . . . . . . . . . . 12 |- ((R e. Top /\ S e. Top) -> (R X.t S) = (topGen` {w | E.u e. R E.v e. S w = (u X. v)}))
44	6, 43	syl5eq 2185	. . . . . . . . . . 11 |- ((R e. Top /\ S e. Top) -> T = (topGen` {w | E.u e. R E.v e. S w = (u X. v)}))
45	44	eleq2d 2211	. . . . . . . . . 10 |- ((R e. Top /\ S e. Top) -> (z e. T <-> z e. (topGen` {w | E.u e. R E.v e. S w = (u X. v)})))
46		txbas 9791	. . . . . . . . . . 11 |- ((R e. Top /\ S e. Top) -> {w | E.u e. R E.v e. S w = (u X. v)} e. TopBases)
47		eltg3 9747	. . . . . . . . . . 11 |- ({w | E.u e. R E.v e. S w = (u X. v)} e. TopBases -> (z e. (topGen` {w | E.u e. R E.v e. S w = (u X. v)}) <-> E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s)))
48	46, 47	syl 13	. . . . . . . . . 10 |- ((R e. Top /\ S e. Top) -> (z e. (topGen` {w | E.u e. R E.v e. S w = (u X. v)}) <-> E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s)))
49	45, 48	bitrd 284	. . . . . . . . 9 |- ((R e. Top /\ S e. Top) -> (z e. T <-> E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s)))
50	49	3adant3 1140	. . . . . . . 8 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (z e. T <-> E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s)))
51	50	adantr 447	. . . . . . 7 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> (z e. T <-> E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s)))
52		imaiun 4935	. . . . . . . . . . 11 |- (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"U.s) = U_t e. s (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t)
53		simpll3 1161	. . . . . . . . . . . 12 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) -> U e. Top)
54		ssel2 2847	. . . . . . . . . . . . . . . 16 |- ((s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ t e. s) -> t e. {w | E.u e. R E.v e. S w = (u X. v)})
55		visset 2541	. . . . . . . . . . . . . . . . 17 |- t e. _V
56		eqeq1 2147	. . . . . . . . . . . . . . . . . 18 |- (w = t -> (w = (u X. v) <-> t = (u X. v)))
57	56	2rexbidv 2391	. . . . . . . . . . . . . . . . 17 |- (w = t -> (E.u e. R E.v e. S w = (u X. v) <-> E.u e. R E.v e. S t = (u X. v)))
58	55, 57	elab 2644	. . . . . . . . . . . . . . . 16 |- (t e. {w | E.u e. R E.v e. S w = (u X. v)} <-> E.u e. R E.v e. S t = (u X. v))
59	54, 58	sylib 242	. . . . . . . . . . . . . . 15 |- ((s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ t e. s) -> E.u e. R E.v e. S t = (u X. v))
60		fveq2 4765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = z -> (F` x) = (F` z))
61		fveq2 4765	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- (x = z -> (G` x) = (G` z))
62	60, 61	opeq12d 3353	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- (x = z -> <.(F` x), (G` x)>. = <.(F` z), (G` z)>.)
63		opex 3690	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- <.(F` z), (G` z)>. e. _V
64	62, 33, 63	fvopab4 4829	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (z e. U.U -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) = <.(F` z), (G` z)>.)
65	64	eleq1d 2210	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (z e. U.U -> (({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v) <-> <.(F` z), (G` z)>. e. (u X. v)))
66		fvex 4778	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (G` z) e. _V
67	66	opelxp 4170	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (<.(F` z), (G` z)>. e. (u X. v) <-> ((F` z) e. u /\ (G` z) e. v))
68	65, 67	syl6bb 729	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (z e. U.U -> (({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v) <-> ((F` z) e. u /\ (G` z) e. v)))
69	68	adantl 448	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) /\ z e. U.U) -> (({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v) <-> ((F` z) e. u /\ (G` z) e. v)))
70	69	pm5.32da 840	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> ((z e. U.U /\ ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v)) <-> (z e. U.U /\ ((F` z) e. u /\ (G` z) e. v))))
71		anandi 887	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((z e. U.U /\ ((F` z) e. u /\ (G` z) e. v)) <-> ((z e. U.U /\ (F` z) e. u) /\ (z e. U.U /\ (G` z) e. v)))
72	70, 71	syl6bb 729	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> ((z e. U.U /\ ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v)) <-> ((z e. U.U /\ (F` z) e. u) /\ (z e. U.U /\ (G` z) e. v))))
73		ffn 4659	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} Fn U.U)
74		elpreima 4869	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} Fn U.U -> (z e. (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) <-> (z e. U.U /\ ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v))))
75	35, 73, 74	3syl 41	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:U.U-->X /\ G:U.U-->Y) -> (z e. (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) <-> (z e. U.U /\ ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v))))
76	75	adantr 447	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> (z e. (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) <-> (z e. U.U /\ ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) e. (u X. v))))
77		elin 2999	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (z e. ((`'F"u) i^i (`'G"v)) <-> (z e. (`'F"u) /\ z e. (`'G"v)))
78		ffn 4659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F:U.U-->X -> F Fn U.U)
79		elpreima 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (F Fn U.U -> (z e. (`'F"u) <-> (z e. U.U /\ (F` z) e. u)))
80	78, 79	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (F:U.U-->X -> (z e. (`'F"u) <-> (z e. U.U /\ (F` z) e. u)))
81		ffn 4659	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (G:U.U-->Y -> G Fn U.U)
82		elpreima 4869	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- (G Fn U.U -> (z e. (`'G"v) <-> (z e. U.U /\ (G` z) e. v)))
83	81, 82	syl 13	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (G:U.U-->Y -> (z e. (`'G"v) <-> (z e. U.U /\ (G` z) e. v)))
84	80, 83	bi2anan9 950	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ((F:U.U-->X /\ G:U.U-->Y) -> ((z e. (`'F"u) /\ z e. (`'G"v)) <-> ((z e. U.U /\ (F` z) e. u) /\ (z e. U.U /\ (G` z) e. v))))
85	77, 84	syl5bb 721	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ((F:U.U-->X /\ G:U.U-->Y) -> (z e. ((`'F"u) i^i (`'G"v)) <-> ((z e. U.U /\ (F` z) e. u) /\ (z e. U.U /\ (G` z) e. v))))
86	85	adantr 447	. . . . . . . . . . . . . . . . . . . . . . 23 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> (z e. ((`'F"u) i^i (`'G"v)) <-> ((z e. U.U /\ (F` z) e. u) /\ (z e. U.U /\ (G` z) e. v))))
87	72, 76, 86	3bitr4d 741	. . . . . . . . . . . . . . . . . . . . . 22 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> (z e. (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) <-> z e. ((`'F"u) i^i (`'G"v))))
88	87	eqrdv 2139	. . . . . . . . . . . . . . . . . . . . 21 |- (((F:U.U-->X /\ G:U.U-->Y) /\ (u e. R /\ v e. S)) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) = ((`'F"u) i^i (`'G"v)))
89	26, 88	sylan 597	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) = ((`'F"u) i^i (`'G"v)))
90		simpll3 1161	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> U e. Top)
91		cnima 9910	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((U e. Top /\ R e. Top /\ F e. (U Cn R)) /\ u e. R) -> (`'F"u) e. U)
92	91	ex 398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((U e. Top /\ R e. Top /\ F e. (U Cn R)) -> (u e. R -> (`'F"u) e. U))
93	92	3expa 1317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((U e. Top /\ R e. Top) /\ F e. (U Cn R)) -> (u e. R -> (`'F"u) e. U))
94	93	ancom1s 856	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((R e. Top /\ U e. Top) /\ F e. (U Cn R)) -> (u e. R -> (`'F"u) e. U))
95	94	3adantl2 1278	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ F e. (U Cn R)) -> (u e. R -> (`'F"u) e. U))
96	95	imp 393	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ F e. (U Cn R)) /\ u e. R) -> (`'F"u) e. U)
97	96	adantlrr 789	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ u e. R) -> (`'F"u) e. U)
98	97	adantrr 781	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> (`'F"u) e. U)
99		cnima 9910	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- (((U e. Top /\ S e. Top /\ G e. (U Cn S)) /\ v e. S) -> (`'G"v) e. U)
100	99	ex 398	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ((U e. Top /\ S e. Top /\ G e. (U Cn S)) -> (v e. S -> (`'G"v) e. U))
101	100	3expa 1317	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- (((U e. Top /\ S e. Top) /\ G e. (U Cn S)) -> (v e. S -> (`'G"v) e. U))
102	101	ancom1s 856	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- (((S e. Top /\ U e. Top) /\ G e. (U Cn S)) -> (v e. S -> (`'G"v) e. U))
103	102	3adantl1 1276	. . . . . . . . . . . . . . . . . . . . . . . 24 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ G e. (U Cn S)) -> (v e. S -> (`'G"v) e. U))
104	103	imp 393	. . . . . . . . . . . . . . . . . . . . . . 23 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ G e. (U Cn S)) /\ v e. S) -> (`'G"v) e. U)
105	104	adantlrl 787	. . . . . . . . . . . . . . . . . . . . . 22 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ v e. S) -> (`'G"v) e. U)
106	105	adantrl 779	. . . . . . . . . . . . . . . . . . . . 21 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> (`'G"v) e. U)
107		inopn 9704	. . . . . . . . . . . . . . . . . . . . 21 |- ((U e. Top /\ (`'F"u) e. U /\ (`'G"v) e. U) -> ((`'F"u) i^i (`'G"v)) e. U)
108	90, 98, 106, 107	syl111anc 1349	. . . . . . . . . . . . . . . . . . . 20 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> ((`'F"u) i^i (`'G"v)) e. U)
109	89, 108	eqeltrd 2218	. . . . . . . . . . . . . . . . . . 19 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (u e. R /\ v e. S)) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) e. U)
110	109	ex 398	. . . . . . . . . . . . . . . . . 18 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ((u e. R /\ v e. S) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) e. U))
111		imaeq2 4380	. . . . . . . . . . . . . . . . . . . 20 |- (t = (u X. v) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) = (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)))
112	111	eleq1d 2210	. . . . . . . . . . . . . . . . . . 19 |- (t = (u X. v) -> ((`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U <-> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) e. U))
113	112	biimprcd 234	. . . . . . . . . . . . . . . . . 18 |- ((`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"(u X. v)) e. U -> (t = (u X. v) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U))
114	110, 113	syl6 42	. . . . . . . . . . . . . . . . 17 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ((u e. R /\ v e. S) -> (t = (u X. v) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)))
115	114	r19.23advv 2466	. . . . . . . . . . . . . . . 16 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> (E.u e. R E.v e. S t = (u X. v) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U))
116	115	imp 393	. . . . . . . . . . . . . . 15 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ E.u e. R E.v e. S t = (u X. v)) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
117	59, 116	sylan2 600	. . . . . . . . . . . . . 14 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ (s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ t e. s)) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
118	117	anassrs 632	. . . . . . . . . . . . 13 |- (((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) /\ t e. s) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
119	118	r19.21aiva 2426	. . . . . . . . . . . 12 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) -> A.t e. s (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
120		iunopn 9703	. . . . . . . . . . . 12 |- ((U e. Top /\ A.t e. s (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U) -> U_t e. s (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
121	53, 119, 120	syl11anc 659	. . . . . . . . . . 11 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) -> U_t e. s (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"t) e. U)
122	52, 121	syl5eqel 2222	. . . . . . . . . 10 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"U.s) e. U)
123		imaeq2 4380	. . . . . . . . . . 11 |- (z = U.s -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) = (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"U.s))
124	123	eleq1d 2210	. . . . . . . . . 10 |- (z = U.s -> ((`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U <-> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"U.s) e. U))
125	122, 124	syl5ibrcom 258	. . . . . . . . 9 |- ((((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) /\ s C_ {w | E.u e. R E.v e. S w = (u X. v)}) -> (z = U.s -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U))
126	125	expimpd 576	. . . . . . . 8 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ((s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U))
127	126	19.23adv 1860	. . . . . . 7 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> (E.s(s C_ {w | E.u e. R E.v e. S w = (u X. v)} /\ z = U.s) -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U))
128	51, 127	sylbid 246	. . . . . 6 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> (z e. T -> (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U))
129	128	r19.21aiv 2425	. . . . 5 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> A.z e. T (`'{<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}"z) e. U)
130	14, 42, 129	mpbir2and 1036	. . . 4 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T))
131	78	adantr 447	. . . . . . . 8 |- ((F:U.U-->X /\ G:U.U-->Y) -> F Fn U.U)
132		fo1st 5138	. . . . . . . . . . . 12 |- 1st:_V-onto->_V
133		fofn 4707	. . . . . . . . . . . 12 |- (1st:_V-onto->_V -> 1st Fn _V)
134	132, 133	ax-mp 7	. . . . . . . . . . 11 |- 1st Fn _V
135		ssv 2864	. . . . . . . . . . 11 |- (X X. Y) C_ _V
136		fnssres 4625	. . . . . . . . . . 11 |- ((1st Fn _V /\ (X X. Y) C_ _V) -> (1st |` (X X. Y)) Fn (X X. Y))
137	134, 135, 136	mp2an 681	. . . . . . . . . 10 |- (1st |` (X X. Y)) Fn (X X. Y)
138	137	a1i 8	. . . . . . . . 9 |- ((F:U.U-->X /\ G:U.U-->Y) -> (1st |` (X X. Y)) Fn (X X. Y))
139	35, 73	syl 13	. . . . . . . . 9 |- ((F:U.U-->X /\ G:U.U-->Y) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} Fn U.U)
140		frn 4665	. . . . . . . . . 10 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y) -> ran {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} C_ (X X. Y))
141	35, 140	syl 13	. . . . . . . . 9 |- ((F:U.U-->X /\ G:U.U-->Y) -> ran {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} C_ (X X. Y))
142		fnco 4620	. . . . . . . . 9 |- (((1st |` (X X. Y)) Fn (X X. Y) /\ {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} Fn U.U /\ ran {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} C_ (X X. Y)) -> ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U)
143	138, 139, 141, 142	syl111anc 1349	. . . . . . . 8 |- ((F:U.U-->X /\ G:U.U-->Y) -> ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U)
144		eqfnfv 4853	. . . . . . . 8 |- ((F Fn U.U /\ ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U) -> (F = ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) <-> (U.U = U.U /\ A.z e. U.U(F` z) = (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))))
145	131, 143, 144	syl11anc 659	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> (F = ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) <-> (U.U = U.U /\ A.z e. U.U(F` z) = (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))))
146		eqidd 2142	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> U.U = U.U)
147		fnfun 4610	. . . . . . . . . . . 12 |- ((1st |` (X X. Y)) Fn (X X. Y) -> Fun (1st |` (X X. Y)))
148	137, 147	ax-mp 7	. . . . . . . . . . 11 |- Fun (1st |` (X X. Y))
149	148	a1i 8	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> Fun (1st |` (X X. Y)))
150	35	adantr 447	. . . . . . . . . . 11 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y))
151		ffun 4661	. . . . . . . . . . 11 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y) -> Fun {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})
152	150, 151	syl 13	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> Fun {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})
153		fdm 4663	. . . . . . . . . . . . 13 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}:U.U-->(X X. Y) -> dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} = U.U)
154	35, 153	syl 13	. . . . . . . . . . . 12 |- ((F:U.U-->X /\ G:U.U-->Y) -> dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} = U.U)
155	154	eleq2d 2211	. . . . . . . . . . 11 |- ((F:U.U-->X /\ G:U.U-->Y) -> (z e. dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} <-> z e. U.U))
156	155	biimpar 616	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> z e. dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})
157		fvco 4822	. . . . . . . . . 10 |- ((Fun (1st |` (X X. Y)) /\ Fun {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} /\ z e. dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) -> (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z) = ((1st |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)))
158	149, 152, 156, 157	syl111anc 1349	. . . . . . . . 9 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z) = ((1st |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)))
159	64	adantl 448	. . . . . . . . . . 11 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z) = <.(F` z), (G` z)>.)
160	159	fveq2d 4769	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((1st |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)) = ((1st |` (X X. Y))` <.(F` z), (G` z)>.))
161		ffvelrn 4877	. . . . . . . . . . . . 13 |- ((F:U.U-->X /\ z e. U.U) -> (F` z) e. X)
162		ffvelrn 4877	. . . . . . . . . . . . 13 |- ((G:U.U-->Y /\ z e. U.U) -> (G` z) e. Y)
163		opelxpi 4173	. . . . . . . . . . . . 13 |- (((F` z) e. X /\ (G` z) e. Y) -> <.(F` z), (G` z)>. e. (X X. Y))
164	161, 162, 163	syl2an 603	. . . . . . . . . . . 12 |- (((F:U.U-->X /\ z e. U.U) /\ (G:U.U-->Y /\ z e. U.U)) -> <.(F` z), (G` z)>. e. (X X. Y))
165	164	anandirs 890	. . . . . . . . . . 11 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> <.(F` z), (G` z)>. e. (X X. Y))
166		fvres 4780	. . . . . . . . . . 11 |- (<.(F` z), (G` z)>. e. (X X. Y) -> ((1st |` (X X. Y))` <.(F` z), (G` z)>.) = (1st` <.(F` z), (G` z)>.))
167	165, 166	syl 13	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((1st |` (X X. Y))` <.(F` z), (G` z)>.) = (1st` <.(F` z), (G` z)>.))
168		fvex 4778	. . . . . . . . . . . 12 |- (F` z) e. _V
169	168	op1st 5132	. . . . . . . . . . 11 |- (1st` <.(F` z), (G` z)>.) = (F` z)
170	169	a1i 8	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (1st` <.(F` z), (G` z)>.) = (F` z))
171	160, 167, 170	3eqtrd 2177	. . . . . . . . 9 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((1st |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)) = (F` z))
172	158, 171	eqtr2d 2174	. . . . . . . 8 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (F` z) = (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))
173	172	r19.21aiva 2426	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> A.z e. U.U(F` z) = (((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))
174	145, 146, 173	mpbir2and 1036	. . . . . 6 |- ((F:U.U-->X /\ G:U.U-->Y) -> F = ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
175		uptx.5	. . . . . . . 8 |- P = (1st |` Z)
176		uptx.4	. . . . . . . . 9 |- Z = (X X. Y)
177	176	reseq2i 4340	. . . . . . . 8 |- (1st |` Z) = (1st |` (X X. Y))
178	175, 177	eqtri 2161	. . . . . . 7 |- P = (1st |` (X X. Y))
179	178	coeq1i 4252	. . . . . 6 |- (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) = ((1st |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})
180	174, 179	syl6eqr 2195	. . . . 5 |- ((F:U.U-->X /\ G:U.U-->Y) -> F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
181	26, 180	syl 13	. . . 4 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
182	81	adantl 448	. . . . . . . 8 |- ((F:U.U-->X /\ G:U.U-->Y) -> G Fn U.U)
183		fo2nd 5139	. . . . . . . . . . . 12 |- 2nd:_V-onto->_V
184		fofn 4707	. . . . . . . . . . . 12 |- (2nd:_V-onto->_V -> 2nd Fn _V)
185	183, 184	ax-mp 7	. . . . . . . . . . 11 |- 2nd Fn _V
186		fnssres 4625	. . . . . . . . . . 11 |- ((2nd Fn _V /\ (X X. Y) C_ _V) -> (2nd |` (X X. Y)) Fn (X X. Y))
187	185, 135, 186	mp2an 681	. . . . . . . . . 10 |- (2nd |` (X X. Y)) Fn (X X. Y)
188	187	a1i 8	. . . . . . . . 9 |- ((F:U.U-->X /\ G:U.U-->Y) -> (2nd |` (X X. Y)) Fn (X X. Y))
189		fnco 4620	. . . . . . . . 9 |- (((2nd |` (X X. Y)) Fn (X X. Y) /\ {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} Fn U.U /\ ran {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} C_ (X X. Y)) -> ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U)
190	188, 139, 141, 189	syl111anc 1349	. . . . . . . 8 |- ((F:U.U-->X /\ G:U.U-->Y) -> ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U)
191		eqfnfv 4853	. . . . . . . 8 |- ((G Fn U.U /\ ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) Fn U.U) -> (G = ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) <-> (U.U = U.U /\ A.z e. U.U(G` z) = (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))))
192	182, 190, 191	syl11anc 659	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> (G = ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) <-> (U.U = U.U /\ A.z e. U.U(G` z) = (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))))
193		fnfun 4610	. . . . . . . . . . . 12 |- ((2nd |` (X X. Y)) Fn (X X. Y) -> Fun (2nd |` (X X. Y)))
194	187, 193	ax-mp 7	. . . . . . . . . . 11 |- Fun (2nd |` (X X. Y))
195	194	a1i 8	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> Fun (2nd |` (X X. Y)))
196		fvco 4822	. . . . . . . . . 10 |- ((Fun (2nd |` (X X. Y)) /\ Fun {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} /\ z e. dom {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) -> (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z) = ((2nd |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)))
197	195, 152, 156, 196	syl111anc 1349	. . . . . . . . 9 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z) = ((2nd |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)))
198	159	fveq2d 4769	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((2nd |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)) = ((2nd |` (X X. Y))` <.(F` z), (G` z)>.))
199		fvres 4780	. . . . . . . . . . 11 |- (<.(F` z), (G` z)>. e. (X X. Y) -> ((2nd |` (X X. Y))` <.(F` z), (G` z)>.) = (2nd` <.(F` z), (G` z)>.))
200	165, 199	syl 13	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((2nd |` (X X. Y))` <.(F` z), (G` z)>.) = (2nd` <.(F` z), (G` z)>.))
201	168, 66	op2nd 5133	. . . . . . . . . . 11 |- (2nd` <.(F` z), (G` z)>.) = (G` z)
202	201	a1i 8	. . . . . . . . . 10 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (2nd` <.(F` z), (G` z)>.) = (G` z))
203	198, 200, 202	3eqtrd 2177	. . . . . . . . 9 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> ((2nd |` (X X. Y))` ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}` z)) = (G` z))
204	197, 203	eqtr2d 2174	. . . . . . . 8 |- (((F:U.U-->X /\ G:U.U-->Y) /\ z e. U.U) -> (G` z) = (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))
205	204	r19.21aiva 2426	. . . . . . 7 |- ((F:U.U-->X /\ G:U.U-->Y) -> A.z e. U.U(G` z) = (((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})` z))
206	192, 146, 205	mpbir2and 1036	. . . . . 6 |- ((F:U.U-->X /\ G:U.U-->Y) -> G = ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
207		uptx.6	. . . . . . . 8 |- Q = (2nd |` Z)
208	176	reseq2i 4340	. . . . . . . 8 |- (2nd |` Z) = (2nd |` (X X. Y))
209	207, 208	eqtri 2161	. . . . . . 7 |- Q = (2nd |` (X X. Y))
210	209	coeq1i 4252	. . . . . 6 |- (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) = ((2nd |` (X X. Y)) o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})
211	206, 210	syl6eqr 2195	. . . . 5 |- ((F:U.U-->X /\ G:U.U-->Y) -> G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
212	26, 211	syl 13	. . . 4 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
213	130, 181, 212	jca32 499	. . 3 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) /\ (F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))))
214		eleq1 2204	. . . . 5 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> (h e. (U Cn T) <-> {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T)))
215		coeq2 4251	. . . . . . 7 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> (P o. h) = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
216	215	eqeq2d 2152	. . . . . 6 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> (F = (P o. h) <-> F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})))
217		coeq2 4251	. . . . . . 7 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> (Q o. h) = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))
218	217	eqeq2d 2152	. . . . . 6 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> (G = (Q o. h) <-> G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})))
219	216, 218	anbi12d 763	. . . . 5 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> ((F = (P o. h) /\ G = (Q o. h)) <-> (F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))))
220	214, 219	anbi12d 763	. . . 4 |- (h = {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} -> ((h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) <-> ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) /\ (F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)})))))
221	220	cla4egv 2605	. . 3 |- ({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. _V -> (({<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)} e. (U Cn T) /\ (F = (P o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}) /\ G = (Q o. {<.x, y>. | (x e. U.U /\ y = <.(F` x), (G` x)>.)}))) -> E.h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h)))))
222	5, 213, 221	sylc 44	. 2 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> E.h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))))
223	25	imdistani 770	. . 3 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> ((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)))
224	8, 9	cnf 9904	. . . . . . . . . . . . 13 |- ((U e. Top /\ T e. Top /\ h e. (U Cn T)) -> h:U.U-->U.T)
225	224	3expia 1319	. . . . . . . . . . . 12 |- ((U e. Top /\ T e. Top) -> (h e. (U Cn T) -> h:U.U-->U.T))
226	7, 225	sylan2 600	. . . . . . . . . . 11 |- ((U e. Top /\ (R e. Top /\ S e. Top)) -> (h e. (U Cn T) -> h:U.U-->U.T))
227	226	ancoms 416	. . . . . . . . . 10 |- (((R e. Top /\ S e. Top) /\ U e. Top) -> (h e. (U Cn T) -> h:U.U-->U.T))
228	227	3impa 1312	. . . . . . . . 9 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (h e. (U Cn T) -> h:U.U-->U.T))
229		feq3 4649	. . . . . . . . . 10 |- (U.T = (X X. Y) -> (h:U.U-->U.T <-> h:U.U-->(X X. Y)))
230	38, 229	syl 13	. . . . . . . . 9 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (h:U.U-->U.T <-> h:U.U-->(X X. Y)))
231	228, 230	sylibd 245	. . . . . . . 8 |- ((R e. Top /\ S e. Top /\ U e. Top) -> (h e. (U Cn T) -> h:U.U-->(X X. Y)))
232	231	adantr 447	. . . . . . 7 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> (h e. (U Cn T) -> h:U.U-->(X X. Y)))
233	232	anim1d 534	. . . . . 6 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> ((h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) -> (h:U.U-->(X X. Y) /\ (F = (P o. h) /\ G = (Q o. h)))))
234		3anass 1106	. . . . . 6 |- ((h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)) <-> (h:U.U-->(X X. Y) /\ (F = (P o. h) /\ G = (Q o. h))))
235	233, 234	syl6ibr 262	. . . . 5 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> ((h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) -> (h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h))))
236	235	19.21aiv 1933	. . . 4 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> A.h((h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) -> (h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h))))
237	178, 209	upxp 11060	. . . . . . . 8 |- ((U.U e. _V /\ F:U.U-->X /\ G:U.U-->Y) -> E!h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
238		eumo 2072	. . . . . . . 8 |- (E!h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)) -> E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
239	237, 238	syl 13	. . . . . . 7 |- ((U.U e. _V /\ F:U.U-->X /\ G:U.U-->Y) -> E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
240	239	3expb 1318	. . . . . 6 |- ((U.U e. _V /\ (F:U.U-->X /\ G:U.U-->Y)) -> E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
241	1, 240	sylan 597	. . . . 5 |- ((U e. Top /\ (F:U.U-->X /\ G:U.U-->Y)) -> E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
242	241	3ad2antl3 1290	. . . 4 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)))
243		immo 2078	. . . 4 |- (A.h((h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) -> (h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h))) -> (E*h(h:U.U-->(X X. Y) /\ F = (P o. h) /\ G = (Q o. h)) -> E*h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h)))))
244	236, 242, 243	sylc 44	. . 3 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F:U.U-->X /\ G:U.U-->Y)) -> E*h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))))
245	223, 244	syl 13	. 2 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> E*h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))))
246		df-reu 2361	. . 3 |- (E!h e. (U Cn T)(F = (P o. h) /\ G = (Q o. h)) <-> E!h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))))
247		eu5 2070	. . 3 |- (E!h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) <-> (E.h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) /\ E*h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h)))))
248	246, 247	bitri 279	. 2 |- (E!h e. (U Cn T)(F = (P o. h) /\ G = (Q o. h)) <-> (E.h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h))) /\ E*h(h e. (U Cn T) /\ (F = (P o. h) /\ G = (Q o. h)))))
249	222, 245, 248	sylanbrc 664	1 |- (((R e. Top /\ S e. Top /\ U e. Top) /\ (F e. (U Cn R) /\ G e. (U Cn S))) -> E!h e. (U Cn T)(F = (P o. h) /\ G = (Q o. h)))

Syntax hints:   -> wi 3   <-> wb 219   /\ wa 337   /\ w3a 1102  A.wal 1584   = wceq 1586   e. wcel 1588  E.wex 1615  E!weu 2037  E*wmo 2038  {cab 2128  A.wral 2355  E.wrex 2356  E!wreu 2357  _Vcvv 2538   i^i cin 2826   C_ wss 2827  <.cop 3240  U.cuni 3366  U_ciun 3436  {copab 3565   X. cxp 4117  `'ccnv 4118  dom cdm 4119  ran crn 4120   |` cres 4121  "cima 4122   o. ccom 4123  Fun wfun 4125   Fn wfn 4126  -->wf 4127  -onto->wfo 4129  ` cfv 4131  (class class class)co 4981  1stc1st 5124  2ndc2nd 5125  Topctop 9686  TopBasesctb 9690  topGenctg 9691   X.t ctx 9788   Cn ccn 9894

This theorem is referenced by:  txcn 11062

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-nul 3083  df-pw 3229  df-sn 3242  df-pr 3243  df-op 3246  df-uni 3367  df-iun 3438  df-br 3508  df-opab 3566  df-id 3747  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-f 4143  df-fo 4145  df-fv 4147  df-opr 4983  df-oprab 4984  df-1st 5126  df-2nd 5127  df-map 5544  df-top 9692  df-bases 9694  df-topgen 9695  df-tx 9789  df-cn 9896

Copyright terms: Public domain