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 𝑆 )
	uptx.2	⊢ 𝑋 = ∪ 𝑅
	uptx.3	⊢ 𝑌 = ∪ 𝑆
	uptx.4	⊢ 𝑍 = ( 𝑋 × 𝑌 )
	uptx.5	⊢ 𝑃 = ( 1^st ↾ 𝑍 )
	uptx.6	⊢ 𝑄 = ( 2^nd ↾ 𝑍 )
Assertion	uptx	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ℎ ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )

Proof

Step	Hyp	Ref	Expression
1		uptx.1	⊢ 𝑇 = ( 𝑅 ×_t 𝑆 )
2		uptx.2	⊢ 𝑋 = ∪ 𝑅
3		uptx.3	⊢ 𝑌 = ∪ 𝑆
4		uptx.4	⊢ 𝑍 = ( 𝑋 × 𝑌 )
5		uptx.5	⊢ 𝑃 = ( 1^st ↾ 𝑍 )
6		uptx.6	⊢ 𝑄 = ( 2^nd ↾ 𝑍 )
7		eqid	⊢ ∪ 𝑈 = ∪ 𝑈
8		eqid	⊢ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ )
9	7 8	txcnmpt	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn ( 𝑅 ×_t 𝑆 ) ) )
10	1	oveq2i	⊢ ( 𝑈 Cn 𝑇 ) = ( 𝑈 Cn ( 𝑅 ×_t 𝑆 ) )
11	9 10	eleqtrrdi	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) )
12	7 2	cnf	⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝐹 : ∪ 𝑈 ⟶ 𝑋 )
13	7 3	cnf	⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝐺 : ∪ 𝑈 ⟶ 𝑌 )
14		ffn	⊢ ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 → 𝐹 Fn ∪ 𝑈 )
15	14	adantr	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐹 Fn ∪ 𝑈 )
16		fo1st	⊢ 1^st : V –onto→ V
17		fofn	⊢ ( 1^st : V –onto→ V → 1^st Fn V )
18	16 17	ax-mp	⊢ 1^st Fn V
19		ssv	⊢ ( 𝑋 × 𝑌 ) ⊆ V
20		fnssres	⊢ ( ( 1^st Fn V ∧ ( 𝑋 × 𝑌 ) ⊆ V ) → ( 1^st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
21	18 19 20	mp2an	⊢ ( 1^st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
22		ffvelcdm	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑥 ∈ ∪ 𝑈 ) → ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 )
23		ffvelcdm	⊢ ( ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑥 ∈ ∪ 𝑈 ) → ( 𝐺 ‘ 𝑥 ) ∈ 𝑌 )
24		opelxpi	⊢ ( ( ( 𝐹 ‘ 𝑥 ) ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑥 ) ∈ 𝑌 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
25	22 23 24	syl2an	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑥 ∈ ∪ 𝑈 ) ∧ ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑥 ∈ ∪ 𝑈 ) ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
26	25	anandirs	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑥 ∈ ∪ 𝑈 ) → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
27	26	fmpttd	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) )
28		ffn	⊢ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) → ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn ∪ 𝑈 )
29	27 28	syl	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn ∪ 𝑈 )
30	27	frnd	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ran ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) )
31		fnco	⊢ ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn ∪ 𝑈 ∧ ran ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn ∪ 𝑈 )
32	21 29 30 31	mp3an2i	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn ∪ 𝑈 )
33		fvco3	⊢ ( ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
34	27 33	sylan	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
35		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
36		fveq2	⊢ ( 𝑥 = 𝑧 → ( 𝐺 ‘ 𝑥 ) = ( 𝐺 ‘ 𝑧 ) )
37	35 36	opeq12d	⊢ ( 𝑥 = 𝑧 → ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ = ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ )
38		opex	⊢ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ V
39	37 8 38	fvmpt	⊢ ( 𝑧 ∈ ∪ 𝑈 → ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ )
40	39	adantl	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) = ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ )
41	40	fveq2d	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
42		ffvelcdm	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐹 ‘ 𝑧 ) ∈ 𝑋 )
43		ffvelcdm	⊢ ( ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) ∈ 𝑌 )
44		opelxpi	⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ 𝑋 ∧ ( 𝐺 ‘ 𝑧 ) ∈ 𝑌 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
45	42 43 44	syl2an	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝑧 ∈ ∪ 𝑈 ) ∧ ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 ∧ 𝑧 ∈ ∪ 𝑈 ) ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
46	45	anandirs	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ∈ ( 𝑋 × 𝑌 ) )
47	46	fvresd	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 1^st ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
48		fvex	⊢ ( 𝐹 ‘ 𝑧 ) ∈ V
49		fvex	⊢ ( 𝐺 ‘ 𝑧 ) ∈ V
50	48 49	op1st	⊢ ( 1^st ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐹 ‘ 𝑧 )
51	47 50	eqtrdi	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐹 ‘ 𝑧 ) )
52	34 41 51	3eqtrrd	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐹 ‘ 𝑧 ) = ( ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
53	15 32 52	eqfnfvd	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐹 = ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
54	4	reseq2i	⊢ ( 1^st ↾ 𝑍 ) = ( 1^st ↾ ( 𝑋 × 𝑌 ) )
55	5 54	eqtri	⊢ 𝑃 = ( 1^st ↾ ( 𝑋 × 𝑌 ) )
56	55	coeq1i	⊢ ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) = ( ( 1^st ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
57	53 56	eqtr4di	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
58	12 13 57	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
59		ffn	⊢ ( 𝐺 : ∪ 𝑈 ⟶ 𝑌 → 𝐺 Fn ∪ 𝑈 )
60	59	adantl	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐺 Fn ∪ 𝑈 )
61		fo2nd	⊢ 2^nd : V –onto→ V
62		fofn	⊢ ( 2^nd : V –onto→ V → 2^nd Fn V )
63	61 62	ax-mp	⊢ 2^nd Fn V
64		fnssres	⊢ ( ( 2^nd Fn V ∧ ( 𝑋 × 𝑌 ) ⊆ V ) → ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) )
65	63 19 64	mp2an	⊢ ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 )
66		fnco	⊢ ( ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) Fn ( 𝑋 × 𝑌 ) ∧ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) Fn ∪ 𝑈 ∧ ran ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ⊆ ( 𝑋 × 𝑌 ) ) → ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn ∪ 𝑈 )
67	65 29 30 66	mp3an2i	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) Fn ∪ 𝑈 )
68		fvco3	⊢ ( ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
69	27 68	sylan	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) = ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) )
70	40	fveq2d	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ‘ 𝑧 ) ) = ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
71	46	fvresd	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 2^nd ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) )
72	48 49	op2nd	⊢ ( 2^nd ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐺 ‘ 𝑧 )
73	71 72	eqtrdi	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ‘ ⟨ ( 𝐹 ‘ 𝑧 ) , ( 𝐺 ‘ 𝑧 ) ⟩ ) = ( 𝐺 ‘ 𝑧 ) )
74	69 70 73	3eqtrrd	⊢ ( ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) ∧ 𝑧 ∈ ∪ 𝑈 ) → ( 𝐺 ‘ 𝑧 ) = ( ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ‘ 𝑧 ) )
75	60 67 74	eqfnfvd	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐺 = ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
76	4	reseq2i	⊢ ( 2^nd ↾ 𝑍 ) = ( 2^nd ↾ ( 𝑋 × 𝑌 ) )
77	6 76	eqtri	⊢ 𝑄 = ( 2^nd ↾ ( 𝑋 × 𝑌 ) )
78	77	coeq1i	⊢ ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) = ( ( 2^nd ↾ ( 𝑋 × 𝑌 ) ) ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) )
79	75 78	eqtr4di	⊢ ( ( 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
80	12 13 79	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
81	11 58 80	jca32	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) ) )
82		eleq1	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ↔ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ) )
83		coeq2	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( 𝑃 ∘ ℎ ) = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
84	83	eqeq2d	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( 𝐹 = ( 𝑃 ∘ ℎ ) ↔ 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) )
85		coeq2	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( 𝑄 ∘ ℎ ) = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) )
86	85	eqeq2d	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( 𝐺 = ( 𝑄 ∘ ℎ ) ↔ 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) )
87	84 86	anbi12d	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ↔ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) ) )
88	82 87	anbi12d	⊢ ( ℎ = ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) → ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ↔ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) ) ) )
89	88	spcegv	⊢ ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) → ( ( ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ∧ 𝐺 = ( 𝑄 ∘ ( 𝑥 ∈ ∪ 𝑈 ↦ ⟨ ( 𝐹 ‘ 𝑥 ) , ( 𝐺 ‘ 𝑥 ) ⟩ ) ) ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
90	11 81 89	sylc	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃ ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
91		eqid	⊢ ∪ 𝑇 = ∪ 𝑇
92	7 91	cnf	⊢ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) → ℎ : ∪ 𝑈 ⟶ ∪ 𝑇 )
93		cntop2	⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑅 ∈ Top )
94		cntop2	⊢ ( 𝐺 ∈ ( 𝑈 Cn 𝑆 ) → 𝑆 ∈ Top )
95	1	unieqi	⊢ ∪ 𝑇 = ∪ ( 𝑅 ×_t 𝑆 )
96	2 3	txuni	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ( 𝑋 × 𝑌 ) = ∪ ( 𝑅 ×_t 𝑆 ) )
97	95 96	eqtr4id	⊢ ( ( 𝑅 ∈ Top ∧ 𝑆 ∈ Top ) → ∪ 𝑇 = ( 𝑋 × 𝑌 ) )
98	93 94 97	syl2an	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∪ 𝑇 = ( 𝑋 × 𝑌 ) )
99	98	feq3d	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ℎ : ∪ 𝑈 ⟶ ∪ 𝑇 ↔ ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ) )
100	92 99	imbitrid	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ℎ ∈ ( 𝑈 Cn 𝑇 ) → ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ) )
101	100	anim1d	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
102		3anass	⊢ ( ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ↔ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
103	101 102	imbitrrdi	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
104	103	alrimiv	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∀ ℎ ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
105		cntop1	⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → 𝑈 ∈ Top )
106	105	uniexd	⊢ ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) → ∪ 𝑈 ∈ V )
107	55 77	upxp	⊢ ( ( ∪ 𝑈 ∈ V ∧ 𝐹 : ∪ 𝑈 ⟶ 𝑋 ∧ 𝐺 : ∪ 𝑈 ⟶ 𝑌 ) → ∃! ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )
108	106 12 13 107	syl2an3an	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )
109		eumo	⊢ ( ∃! ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) → ∃* ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )
110	108 109	syl	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃* ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )
111		moim	⊢ ( ∀ ℎ ( ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) → ( ∃* ℎ ( ℎ : ∪ 𝑈 ⟶ ( 𝑋 × 𝑌 ) ∧ 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) → ∃* ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
112	104 110 111	sylc	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃* ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
113		df-reu	⊢ ( ∃! ℎ ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ↔ ∃! ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) )
114		df-eu	⊢ ( ∃! ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ↔ ( ∃ ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ ∃* ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
115	113 114	bitri	⊢ ( ∃! ℎ ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ↔ ( ∃ ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ∧ ∃* ℎ ( ℎ ∈ ( 𝑈 Cn 𝑇 ) ∧ ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) ) ) )
116	90 112 115	sylanbrc	⊢ ( ( 𝐹 ∈ ( 𝑈 Cn 𝑅 ) ∧ 𝐺 ∈ ( 𝑈 Cn 𝑆 ) ) → ∃! ℎ ∈ ( 𝑈 Cn 𝑇 ) ( 𝐹 = ( 𝑃 ∘ ℎ ) ∧ 𝐺 = ( 𝑄 ∘ ℎ ) ) )

Metamath Proof Explorer

Theorem uptx

Proof