MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uptx Structured version   Visualization version   GIF version
Theorem uptx 23362
Description: Universal property of the binary topological product. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 22-Aug-2015.)
Hypotheses
Ref Expression
uptx.1 š‘‡ = (š‘… Ɨt š‘†)
uptx.2 š‘‹ = āˆŖ š‘…
uptx.3 š‘Œ = āˆŖ š‘†
uptx.4 š‘ = (š‘‹ Ɨ š‘Œ)
uptx.5 š‘ƒ = (1st ā†¾ š‘)
uptx.6 š‘„ = (2nd ā†¾ š‘)
Assertion
Ref Expression
uptx ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Distinct variable groups:   ā„Ž,š¹   ā„Ž,šŗ   š‘ƒ,ā„Ž   š‘„,ā„Ž   š‘…,ā„Ž   š‘‡,ā„Ž   š‘†,ā„Ž   š‘ˆ,ā„Ž   ā„Ž,š‘‹   ā„Ž,š‘Œ
Allowed substitution hint:   š‘(ā„Ž)
Proof of Theorem uptx
Dummy variables š‘„ š‘§ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2731 . . . . 5 āˆŖ š‘ˆ = āˆŖ š‘ˆ
2 eqid 2731 . . . . 5 (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)
31, 2txcnmpt 23361 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn (š‘… Ɨt š‘†)))
4 uptx.1 . . . . 5 š‘‡ = (š‘… Ɨt š‘†)
54oveq2i 7423 . . . 4 (š‘ˆ Cn š‘‡) = (š‘ˆ Cn (š‘… Ɨt š‘†))
63, 5eleqtrrdi 2843 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡))
7 uptx.2 . . . . . 6 š‘‹ = āˆŖ š‘…
81, 7cnf 22983 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
9 uptx.3 . . . . . 6 š‘Œ = āˆŖ š‘†
101, 9cnf 22983 . . . . 5 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
11 ffn 6717 . . . . . . . 8 (š¹:āˆŖ š‘ˆāŸ¶š‘‹ ā†’ š¹ Fn āˆŖ š‘ˆ)
1211adantr 480 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ Fn āˆŖ š‘ˆ)
13 fo1st 7999 . . . . . . . . . 10 1st :Vā€“ontoā†’V
14 fofn 6807 . . . . . . . . . 10 (1st :Vā€“ontoā†’V ā†’ 1st Fn V)
1513, 14ax-mp 5 . . . . . . . . 9 1st Fn V
16 ssv 4006 . . . . . . . . 9 (š‘‹ Ɨ š‘Œ) āŠ† V
17 fnssres 6673 . . . . . . . . 9 ((1st Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
1815, 16, 17mp2an 689 . . . . . . . 8 (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
19 ffvelcdm 7083 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘„) āˆˆ š‘‹)
20 ffvelcdm 7083 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘„) āˆˆ š‘Œ)
21 opelxpi 5713 . . . . . . . . . . . 12 (((š¹ā€˜š‘„) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘„) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2219, 20, 21syl2an 595 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2322anandirs 676 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2423fmpttd 7116 . . . . . . . . 9 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ))
25 ffn 6717 . . . . . . . . 9 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2624, 25syl 17 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2724frnd 6725 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ))
28 fnco 6667 . . . . . . . 8 (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
2918, 26, 27, 28mp3an2i 1465 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
30 fvco3 6990 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
3124, 30sylan 579 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
32 fveq2 6891 . . . . . . . . . . . 12 (š‘„ = š‘§ ā†’ (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
33 fveq2 6891 . . . . . . . . . . . 12 (š‘„ = š‘§ ā†’ (šŗā€˜š‘„) = (šŗā€˜š‘§))
3432, 33opeq12d 4881 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
35 opex 5464 . . . . . . . . . . 11 āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ V
3634, 2, 35fvmpt 6998 . . . . . . . . . 10 (š‘§ āˆˆ āˆŖ š‘ˆ ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
3736adantl 481 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
3837fveq2d 6895 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
39 ffvelcdm 7083 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
40 ffvelcdm 7083 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
41 opelxpi 5713 . . . . . . . . . . . 12 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4239, 40, 41syl2an 595 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4342anandirs 676 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4443fvresd 6911 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
45 fvex 6904 . . . . . . . . . 10 (š¹ā€˜š‘§) āˆˆ V
46 fvex 6904 . . . . . . . . . 10 (šŗā€˜š‘§) āˆˆ V
4745, 46op1st 7987 . . . . . . . . 9 (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§)
4844, 47eqtrdi 2787 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
4931, 38, 483eqtrrd 2776 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
5012, 29, 49eqfnfvd 7035 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
51 uptx.5 . . . . . . . 8 š‘ƒ = (1st ā†¾ š‘)
52 uptx.4 . . . . . . . . 9 š‘ = (š‘‹ Ɨ š‘Œ)
5352reseq2i 5978 . . . . . . . 8 (1st ā†¾ š‘) = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5451, 53eqtri 2759 . . . . . . 7 š‘ƒ = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5554coeq1i 5859 . . . . . 6 (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
5650, 55eqtr4di 2789 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
578, 10, 56syl2an 595 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
58 ffn 6717 . . . . . . . 8 (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ ā†’ šŗ Fn āˆŖ š‘ˆ)
5958adantl 481 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ Fn āˆŖ š‘ˆ)
60 fo2nd 8000 . . . . . . . . . 10 2nd :Vā€“ontoā†’V
61 fofn 6807 . . . . . . . . . 10 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
6260, 61ax-mp 5 . . . . . . . . 9 2nd Fn V
63 fnssres 6673 . . . . . . . . 9 ((2nd Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
6462, 16, 63mp2an 689 . . . . . . . 8 (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
65 fnco 6667 . . . . . . . 8 (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
6664, 26, 27, 65mp3an2i 1465 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
67 fvco3 6990 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
6824, 67sylan 579 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
6937fveq2d 6895 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7043fvresd 6911 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7145, 46op2nd 7988 . . . . . . . . 9 (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§)
7270, 71eqtrdi 2787 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7368, 69, 723eqtrrd 2776 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
7459, 66, 73eqfnfvd 7035 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
75 uptx.6 . . . . . . . 8 š‘„ = (2nd ā†¾ š‘)
7652reseq2i 5978 . . . . . . . 8 (2nd ā†¾ š‘) = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
7775, 76eqtri 2759 . . . . . . 7 š‘„ = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
7877coeq1i 5859 . . . . . 6 (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
7974, 78eqtr4di 2789 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
808, 10, 79syl2an 595 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
816, 57, 80jca32 515 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
82 eleq1 2820 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†” (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡)))
83 coeq2 5858 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘ƒ āˆ˜ ā„Ž) = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8483eqeq2d 2742 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†” š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
85 coeq2 5858 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘„ āˆ˜ ā„Ž) = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8685eqeq2d 2742 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (šŗ = (š‘„ āˆ˜ ā„Ž) ā†” šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
8784, 86anbi12d 630 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
8882, 87anbi12d 630 . . . 4 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))))
8988spcegv 3587 . . 3 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) ā†’ (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
906, 81, 89sylc 65 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
91 eqid 2731 . . . . . . . 8 āˆŖ š‘‡ = āˆŖ š‘‡
921, 91cnf 22983 . . . . . . 7 (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡)
93 cntop2 22978 . . . . . . . . 9 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘… āˆˆ Top)
94 cntop2 22978 . . . . . . . . 9 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ š‘† āˆˆ Top)
954unieqi 4921 . . . . . . . . . 10 āˆŖ š‘‡ = āˆŖ (š‘… Ɨt š‘†)
967, 9txuni 23329 . . . . . . . . . 10 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ (š‘‹ Ɨ š‘Œ) = āˆŖ (š‘… Ɨt š‘†))
9795, 96eqtr4id 2790 . . . . . . . . 9 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
9893, 94, 97syl2an 595 . . . . . . . 8 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
9998feq3d 6704 . . . . . . 7 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡ ā†” ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
10092, 99imbitrid 243 . . . . . 6 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
101100anim1d 610 . . . . 5 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
102 3anass 1094 . . . . 5 ((ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
103101, 102imbitrrdi 251 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
104103alrimiv 1929 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
105 cntop1 22977 . . . . . 6 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘ˆ āˆˆ Top)
106105uniexd 7736 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ āˆŖ š‘ˆ āˆˆ V)
10754, 77upxp 23360 . . . . 5 ((āˆŖ š‘ˆ āˆˆ V āˆ§ š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
108106, 8, 10, 107syl2an3an 1421 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
109 eumo 2571 . . . 4 (āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
110108, 109syl 17 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
111 moim 2537 . . 3 (āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
112104, 110, 111sylc 65 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
113 df-reu 3376 . . 3 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
114 df-eu 2562 . . 3 (āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
115113, 114bitri 275 . 2 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
11690, 112, 115sylanbrc 582 1 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Colors of variables: wff setvar class
Syntax hints:   ā†’ wi 4   āˆ§ wa 395   āˆ§ w3a 1086  āˆ€wal 1538   = wceq 1540  āˆƒwex 1780   āˆˆ wcel 2105  āˆƒ*wmo 2531  āˆƒ!weu 2561  āˆƒ!wreu 3373  Vcvv 3473   āŠ† wss 3948  āŸØcop 4634  āˆŖ cuni 4908   ā†¦ cmpt 5231   Ɨ cxp 5674  ran crn 5677   ā†¾ cres 5678   āˆ˜ ccom 5680   Fn wfn 6538  āŸ¶wf 6539  ā€“ontoā†’wfo 6541  ā€˜cfv 6543  (class class class)co 7412  1st c1st 7977  2nd c2nd 7978  Topctop 22628   Cn ccn 22961   Ɨt ctx 23297
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-ral 3061  df-rex 3070  df-reu 3376  df-rab 3432  df-v 3475  df-sbc 3778  df-csb 3894  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-pw 4604  df-sn 4629  df-pr 4631  df-op 4635  df-uni 4909  df-iun 4999  df-br 5149  df-opab 5211  df-mpt 5232  df-id 5574  df-xp 5682  df-rel 5683  df-cnv 5684  df-co 5685  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-iota 6495  df-fun 6545  df-fn 6546  df-f 6547  df-f1 6548  df-fo 6549  df-f1o 6550  df-fv 6551  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7979  df-2nd 7980  df-map 8828  df-topgen 17396  df-top 22629  df-topon 22646  df-bases 22682  df-cn 22964  df-tx 23299
This theorem is referenced by:  txcn  23363
  Copyright terms: Public domain W3C validator