uptx

Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 22-Aug-2015)

	Ref	Expression
Hypotheses	uptx.1	$⊢ T = R \times_{t} S$
	uptx.2	$⊢ X = ⋃ R$
	uptx.3	$⊢ Y = ⋃ S$
	uptx.4	$⊢ Z = X \times Y$
	uptx.5	$⊢ P = {1^{st} ↾}_{Z}$
	uptx.6	$⊢ Q = {2^{nd} ↾}_{Z}$
Assertion	uptx	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists! h \in (U Cn T) (F = P \circ h \land G = Q \circ h)$

Proof

Step	Hyp	Ref	Expression
1		uptx.1	$⊢ T = R \times_{t} S$
2		uptx.2	$⊢ X = ⋃ R$
3		uptx.3	$⊢ Y = ⋃ S$
4		uptx.4	$⊢ Z = X \times Y$
5		uptx.5	$⊢ P = {1^{st} ↾}_{Z}$
6		uptx.6	$⊢ Q = {2^{nd} ↾}_{Z}$
7		eqid	$⊢ ⋃ U = ⋃ U$
8		eqid	$⊢ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
9	7 8	txcnmpt	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn (R \times_{t} S))$
10	1	oveq2i	$⊢ U Cn T = U Cn (R \times_{t} S)$
11	9 10	eleqtrrdi	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T)$
12	7 2	cnf	$⊢ F \in (U Cn R) \to F : ⋃ U ⟶ X$
13	7 3	cnf	$⊢ G \in (U Cn S) \to G : ⋃ U ⟶ Y$
14		ffn	$⊢ F : ⋃ U ⟶ X \to F Fn ⋃ U$
15	14	adantr	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to F Fn ⋃ U$
16		fo1st	$⊢ 1^{st} : V \underset{onto}{⟶} V$
17		fofn	$⊢ 1^{st} : V \underset{onto}{⟶} V \to 1^{st} Fn V$
18	16 17	ax-mp	$⊢ 1^{st} Fn V$
19		ssv	$⊢ X \times Y \subseteq V$
20		fnssres	$⊢ (1^{st} Fn V \land X \times Y \subseteq V) \to ({1^{st} ↾}_{(X \times Y)}) Fn (X \times Y)$
21	18 19 20	mp2an	$⊢ ({1^{st} ↾}_{(X \times Y)}) Fn (X \times Y)$
22		ffvelrn	$⊢ (F : ⋃ U ⟶ X \land x \in ⋃ U) \to F (x) \in X$
23		ffvelrn	$⊢ (G : ⋃ U ⟶ Y \land x \in ⋃ U) \to G (x) \in Y$
24		opelxpi	$⊢ (F (x) \in X \land G (x) \in Y) \to ⟨F (x), G (x)⟩ \in (X \times Y)$
25	22 23 24	syl2an	$⊢ ((F : ⋃ U ⟶ X \land x \in ⋃ U) \land (G : ⋃ U ⟶ Y \land x \in ⋃ U)) \to ⟨F (x), G (x)⟩ \in (X \times Y)$
26	25	anandirs	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land x \in ⋃ U) \to ⟨F (x), G (x)⟩ \in (X \times Y)$
27	26	fmpttd	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) : ⋃ U ⟶ X \times Y$
28		ffn	$⊢ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) : ⋃ U ⟶ X \times Y \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) Fn ⋃ U$
29	27 28	syl	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) Fn ⋃ U$
30	27	frnd	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to ran (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \subseteq X \times Y$
31		fnco	$⊢ (({1^{st} ↾}_{(X \times Y)}) Fn (X \times Y) \land (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) Fn ⋃ U \land ran (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \subseteq X \times Y) \to (({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) Fn ⋃ U$
32	21 29 30 31	mp3an2i	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to (({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) Fn ⋃ U$
33		fvco3	$⊢ ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) : ⋃ U ⟶ X \times Y \land z \in ⋃ U) \to (({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z) = ({1^{st} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z))$
34	27 33	sylan	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to (({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z) = ({1^{st} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z))$
35		fveq2	$⊢ x = z \to F (x) = F (z)$
36		fveq2	$⊢ x = z \to G (x) = G (z)$
37	35 36	opeq12d	$⊢ x = z \to ⟨F (x), G (x)⟩ = ⟨F (z), G (z)⟩$
38		opex	$⊢ ⟨F (z), G (z)⟩ \in V$
39	37 8 38	fvmpt	$⊢ z \in ⋃ U \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z) = ⟨F (z), G (z)⟩$
40	39	adantl	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z) = ⟨F (z), G (z)⟩$
41	40	fveq2d	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({1^{st} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z)) = ({1^{st} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩)$
42		ffvelrn	$⊢ (F : ⋃ U ⟶ X \land z \in ⋃ U) \to F (z) \in X$
43		ffvelrn	$⊢ (G : ⋃ U ⟶ Y \land z \in ⋃ U) \to G (z) \in Y$
44		opelxpi	$⊢ (F (z) \in X \land G (z) \in Y) \to ⟨F (z), G (z)⟩ \in (X \times Y)$
45	42 43 44	syl2an	$⊢ ((F : ⋃ U ⟶ X \land z \in ⋃ U) \land (G : ⋃ U ⟶ Y \land z \in ⋃ U)) \to ⟨F (z), G (z)⟩ \in (X \times Y)$
46	45	anandirs	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ⟨F (z), G (z)⟩ \in (X \times Y)$
47	46	fvresd	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({1^{st} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩) = 1^{st} (⟨F (z), G (z)⟩)$
48		fvex	$⊢ F (z) \in V$
49		fvex	$⊢ G (z) \in V$
50	48 49	op1st	$⊢ 1^{st} (⟨F (z), G (z)⟩) = F (z)$
51	47 50	eqtrdi	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({1^{st} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩) = F (z)$
52	34 41 51	3eqtrrd	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to F (z) = (({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z)$
53	15 32 52	eqfnfvd	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to F = ({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
54	4	reseq2i	$⊢ {1^{st} ↾}_{Z} = {1^{st} ↾}_{(X \times Y)}$
55	5 54	eqtri	$⊢ P = {1^{st} ↾}_{(X \times Y)}$
56	55	coeq1i	$⊢ P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) = ({1^{st} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
57	53 56	eqtr4di	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
58	12 13 57	syl2an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
59		ffn	$⊢ G : ⋃ U ⟶ Y \to G Fn ⋃ U$
60	59	adantl	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to G Fn ⋃ U$
61		fo2nd	$⊢ 2^{nd} : V \underset{onto}{⟶} V$
62		fofn	$⊢ 2^{nd} : V \underset{onto}{⟶} V \to 2^{nd} Fn V$
63	61 62	ax-mp	$⊢ 2^{nd} Fn V$
64		fnssres	$⊢ (2^{nd} Fn V \land X \times Y \subseteq V) \to ({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y)$
65	63 19 64	mp2an	$⊢ ({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y)$
66		fnco	$⊢ (({2^{nd} ↾}_{(X \times Y)}) Fn (X \times Y) \land (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) Fn ⋃ U \land ran (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \subseteq X \times Y) \to (({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) Fn ⋃ U$
67	65 29 30 66	mp3an2i	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to (({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) Fn ⋃ U$
68		fvco3	$⊢ ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) : ⋃ U ⟶ X \times Y \land z \in ⋃ U) \to (({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z) = ({2^{nd} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z))$
69	27 68	sylan	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to (({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z) = ({2^{nd} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z))$
70	40	fveq2d	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({2^{nd} ↾}_{(X \times Y)}) ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) (z)) = ({2^{nd} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩)$
71	46	fvresd	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({2^{nd} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩) = 2^{nd} (⟨F (z), G (z)⟩)$
72	48 49	op2nd	$⊢ 2^{nd} (⟨F (z), G (z)⟩) = G (z)$
73	71 72	eqtrdi	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to ({2^{nd} ↾}_{(X \times Y)}) (⟨F (z), G (z)⟩) = G (z)$
74	69 70 73	3eqtrrd	$⊢ ((F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \land z \in ⋃ U) \to G (z) = (({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)) (z)$
75	60 67 74	eqfnfvd	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to G = ({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
76	4	reseq2i	$⊢ {2^{nd} ↾}_{Z} = {2^{nd} ↾}_{(X \times Y)}$
77	6 76	eqtri	$⊢ Q = {2^{nd} ↾}_{(X \times Y)}$
78	77	coeq1i	$⊢ Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) = ({2^{nd} ↾}_{(X \times Y)}) \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
79	75 78	eqtr4di	$⊢ (F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
80	12 13 79	syl2an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
81	11 58 80	jca32	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T) \land (F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)))$
82		eleq1	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to (h \in (U Cn T) \leftrightarrow (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T))$
83		coeq2	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to P \circ h = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
84	83	eqeq2d	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to (F = P \circ h \leftrightarrow F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩))$
85		coeq2	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to Q \circ h = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)$
86	85	eqeq2d	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to (G = Q \circ h \leftrightarrow G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩))$
87	84 86	anbi12d	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to ((F = P \circ h \land G = Q \circ h) \leftrightarrow (F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩)))$
88	82 87	anbi12d	$⊢ h = (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \to ((h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \leftrightarrow ((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T) \land (F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩))))$
89	88	spcegv	$⊢ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T) \to (((x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \in (U Cn T) \land (F = P \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩) \land G = Q \circ (x \in ⋃ U ⟼ ⟨F (x), G (x)⟩))) \to \exists h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)))$
90	11 81 89	sylc	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h))$
91		eqid	$⊢ ⋃ T = ⋃ T$
92	7 91	cnf	$⊢ h \in (U Cn T) \to h : ⋃ U ⟶ ⋃ T$
93		cntop2	$⊢ F \in (U Cn R) \to R \in Top$
94		cntop2	$⊢ G \in (U Cn S) \to S \in Top$
95	1	unieqi	$⊢ ⋃ T = ⋃ (R \times_{t} S)$
96	2 3	txuni	$⊢ (R \in Top \land S \in Top) \to X \times Y = ⋃ (R \times_{t} S)$
97	95 96	eqtr4id	$⊢ (R \in Top \land S \in Top) \to ⋃ T = X \times Y$
98	93 94 97	syl2an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to ⋃ T = X \times Y$
99	98	feq3d	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to (h : ⋃ U ⟶ ⋃ T \leftrightarrow h : ⋃ U ⟶ X \times Y)$
100	92 99	syl5ib	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to (h \in (U Cn T) \to h : ⋃ U ⟶ X \times Y)$
101	100	anim1d	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to ((h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \to (h : ⋃ U ⟶ X \times Y \land (F = P \circ h \land G = Q \circ h)))$
102		3anass	$⊢ (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h) \leftrightarrow (h : ⋃ U ⟶ X \times Y \land (F = P \circ h \land G = Q \circ h))$
103	101 102	syl6ibr	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to ((h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \to (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h))$
104	103	alrimiv	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \forall h ((h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \to (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h))$
105		cntop1	$⊢ F \in (U Cn R) \to U \in Top$
106	105	uniexd	$⊢ F \in (U Cn R) \to ⋃ U \in V$
107	55 77	upxp	$⊢ (⋃ U \in V \land F : ⋃ U ⟶ X \land G : ⋃ U ⟶ Y) \to \exists! h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h)$
108	106 12 13 107	syl2an3an	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists! h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h)$
109		eumo	$⊢ \exists! h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h) \to \exists^{*} h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h)$
110	108 109	syl	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists^{*} h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h)$
111		moim	$⊢ \forall h ((h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \to (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h)) \to (\exists^{} h (h : ⋃ U ⟶ X \times Y \land F = P \circ h \land G = Q \circ h) \to \exists^{} h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)))$
112	104 110 111	sylc	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists^{*} h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h))$
113		df-reu	$⊢ \exists! h \in (U Cn T) (F = P \circ h \land G = Q \circ h) \leftrightarrow \exists! h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h))$
114		df-eu	$⊢ \exists! h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \leftrightarrow (\exists h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \land \exists^{*} h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)))$
115	113 114	bitri	$⊢ \exists! h \in (U Cn T) (F = P \circ h \land G = Q \circ h) \leftrightarrow (\exists h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)) \land \exists^{*} h (h \in (U Cn T) \land (F = P \circ h \land G = Q \circ h)))$
116	90 112 115	sylanbrc	$⊢ (F \in (U Cn R) \land G \in (U Cn S)) \to \exists! h \in (U Cn T) (F = P \circ h \land G = Q \circ h)$

Metamath Proof Explorer

Theorem uptx

Proof