MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  uptx Structured version   Visualization version   GIF version
Theorem uptx 23121
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 2733 . . . . 5 āˆŖ š‘ˆ = āˆŖ š‘ˆ
2 eqid 2733 . . . . 5 (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)
31, 2txcnmpt 23120 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn (š‘… Ɨt š‘†)))
4 uptx.1 . . . . 5 š‘‡ = (š‘… Ɨt š‘†)
54oveq2i 7417 . . . 4 (š‘ˆ Cn š‘‡) = (š‘ˆ Cn (š‘… Ɨt š‘†))
63, 5eleqtrrdi 2845 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡))
7 uptx.2 . . . . . 6 š‘‹ = āˆŖ š‘…
81, 7cnf 22742 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
9 uptx.3 . . . . . 6 š‘Œ = āˆŖ š‘†
101, 9cnf 22742 . . . . 5 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
11 ffn 6715 . . . . . . . 8 (š¹:āˆŖ š‘ˆāŸ¶š‘‹ ā†’ š¹ Fn āˆŖ š‘ˆ)
1211adantr 482 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ Fn āˆŖ š‘ˆ)
13 fo1st 7992 . . . . . . . . . 10 1st :Vā€“ontoā†’V
14 fofn 6805 . . . . . . . . . 10 (1st :Vā€“ontoā†’V ā†’ 1st Fn V)
1513, 14ax-mp 5 . . . . . . . . 9 1st Fn V
16 ssv 4006 . . . . . . . . 9 (š‘‹ Ɨ š‘Œ) āŠ† V
17 fnssres 6671 . . . . . . . . 9 ((1st Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
1815, 16, 17mp2an 691 . . . . . . . 8 (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
19 ffvelcdm 7081 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘„) āˆˆ š‘‹)
20 ffvelcdm 7081 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘„) āˆˆ š‘Œ)
21 opelxpi 5713 . . . . . . . . . . . 12 (((š¹ā€˜š‘„) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘„) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2219, 20, 21syl2an 597 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2322anandirs 678 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2423fmpttd 7112 . . . . . . . . 9 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ))
25 ffn 6715 . . . . . . . . 9 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2624, 25syl 17 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2724frnd 6723 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ))
28 fnco 6665 . . . . . . . 8 (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
2918, 26, 27, 28mp3an2i 1467 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
30 fvco3 6988 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
3124, 30sylan 581 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
32 fveq2 6889 . . . . . . . . . . . 12 (š‘„ = š‘§ ā†’ (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
33 fveq2 6889 . . . . . . . . . . . 12 (š‘„ = š‘§ ā†’ (šŗā€˜š‘„) = (šŗā€˜š‘§))
3432, 33opeq12d 4881 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
35 opex 5464 . . . . . . . . . . 11 āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ V
3634, 2, 35fvmpt 6996 . . . . . . . . . 10 (š‘§ āˆˆ āˆŖ š‘ˆ ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
3736adantl 483 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
3837fveq2d 6893 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
39 ffvelcdm 7081 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
40 ffvelcdm 7081 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
41 opelxpi 5713 . . . . . . . . . . . 12 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4239, 40, 41syl2an 597 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4342anandirs 678 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4443fvresd 6909 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
45 fvex 6902 . . . . . . . . . 10 (š¹ā€˜š‘§) āˆˆ V
46 fvex 6902 . . . . . . . . . 10 (šŗā€˜š‘§) āˆˆ V
4745, 46op1st 7980 . . . . . . . . 9 (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§)
4844, 47eqtrdi 2789 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
4931, 38, 483eqtrrd 2778 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
5012, 29, 49eqfnfvd 7033 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
51 uptx.5 . . . . . . . 8 š‘ƒ = (1st ā†¾ š‘)
52 uptx.4 . . . . . . . . 9 š‘ = (š‘‹ Ɨ š‘Œ)
5352reseq2i 5977 . . . . . . . 8 (1st ā†¾ š‘) = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5451, 53eqtri 2761 . . . . . . 7 š‘ƒ = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5554coeq1i 5858 . . . . . 6 (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
5650, 55eqtr4di 2791 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
578, 10, 56syl2an 597 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
58 ffn 6715 . . . . . . . 8 (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ ā†’ šŗ Fn āˆŖ š‘ˆ)
5958adantl 483 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ Fn āˆŖ š‘ˆ)
60 fo2nd 7993 . . . . . . . . . 10 2nd :Vā€“ontoā†’V
61 fofn 6805 . . . . . . . . . 10 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
6260, 61ax-mp 5 . . . . . . . . 9 2nd Fn V
63 fnssres 6671 . . . . . . . . 9 ((2nd Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
6462, 16, 63mp2an 691 . . . . . . . 8 (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
65 fnco 6665 . . . . . . . 8 (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
6664, 26, 27, 65mp3an2i 1467 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
67 fvco3 6988 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
6824, 67sylan 581 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
6937fveq2d 6893 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7043fvresd 6909 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7145, 46op2nd 7981 . . . . . . . . 9 (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§)
7270, 71eqtrdi 2789 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7368, 69, 723eqtrrd 2778 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
7459, 66, 73eqfnfvd 7033 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
75 uptx.6 . . . . . . . 8 š‘„ = (2nd ā†¾ š‘)
7652reseq2i 5977 . . . . . . . 8 (2nd ā†¾ š‘) = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
7775, 76eqtri 2761 . . . . . . 7 š‘„ = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
7877coeq1i 5858 . . . . . 6 (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
7974, 78eqtr4di 2791 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
808, 10, 79syl2an 597 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
816, 57, 80jca32 517 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
82 eleq1 2822 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†” (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡)))
83 coeq2 5857 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘ƒ āˆ˜ ā„Ž) = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8483eqeq2d 2744 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†” š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
85 coeq2 5857 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘„ āˆ˜ ā„Ž) = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8685eqeq2d 2744 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (šŗ = (š‘„ āˆ˜ ā„Ž) ā†” šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
8784, 86anbi12d 632 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
8882, 87anbi12d 632 . . . 4 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))))
8988spcegv 3588 . . 3 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) ā†’ (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
906, 81, 89sylc 65 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
91 eqid 2733 . . . . . . . 8 āˆŖ š‘‡ = āˆŖ š‘‡
921, 91cnf 22742 . . . . . . 7 (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡)
93 cntop2 22737 . . . . . . . . 9 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘… āˆˆ Top)
94 cntop2 22737 . . . . . . . . 9 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ š‘† āˆˆ Top)
954unieqi 4921 . . . . . . . . . 10 āˆŖ š‘‡ = āˆŖ (š‘… Ɨt š‘†)
967, 9txuni 23088 . . . . . . . . . 10 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ (š‘‹ Ɨ š‘Œ) = āˆŖ (š‘… Ɨt š‘†))
9795, 96eqtr4id 2792 . . . . . . . . 9 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
9893, 94, 97syl2an 597 . . . . . . . 8 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
9998feq3d 6702 . . . . . . 7 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡ ā†” ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
10092, 99imbitrid 243 . . . . . 6 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
101100anim1d 612 . . . . 5 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
102 3anass 1096 . . . . 5 ((ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
103101, 102syl6ibr 252 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
104103alrimiv 1931 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
105 cntop1 22736 . . . . . 6 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘ˆ āˆˆ Top)
106105uniexd 7729 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ āˆŖ š‘ˆ āˆˆ V)
10754, 77upxp 23119 . . . . 5 ((āˆŖ š‘ˆ āˆˆ V āˆ§ š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
108106, 8, 10, 107syl2an3an 1423 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
109 eumo 2573 . . . 4 (āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
110108, 109syl 17 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
111 moim 2539 . . 3 (āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
112104, 110, 111sylc 65 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
113 df-reu 3378 . . 3 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
114 df-eu 2564 . . 3 (āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
115113, 114bitri 275 . 2 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
11690, 112, 115sylanbrc 584 1 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Colors of variables: wff setvar class
Syntax hints:   ā†’ wi 4   āˆ§ wa 397   āˆ§ w3a 1088  āˆ€wal 1540   = wceq 1542  āˆƒwex 1782   āˆˆ wcel 2107  āˆƒ*wmo 2533  āˆƒ!weu 2563  āˆƒ!wreu 3375  Vcvv 3475   āŠ† wss 3948  āŸØcop 4634  āˆŖ cuni 4908   ā†¦ cmpt 5231   Ɨ cxp 5674  ran crn 5677   ā†¾ cres 5678   āˆ˜ ccom 5680   Fn wfn 6536  āŸ¶wf 6537  ā€“ontoā†’wfo 6539  ā€˜cfv 6541  (class class class)co 7406  1st c1st 7970  2nd c2nd 7971  Topctop 22387   Cn ccn 22720   Ɨt ctx 23056
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-rep 5285  ax-sep 5299  ax-nul 5306  ax-pow 5363  ax-pr 5427  ax-un 7722
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2535  df-eu 2564  df-clab 2711  df-cleq 2725  df-clel 2811  df-nfc 2886  df-ne 2942  df-ral 3063  df-rex 3072  df-reu 3378  df-rab 3434  df-v 3477  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 6493  df-fun 6543  df-fn 6544  df-f 6545  df-f1 6546  df-fo 6547  df-f1o 6548  df-fv 6549  df-ov 7409  df-oprab 7410  df-mpo 7411  df-1st 7972  df-2nd 7973  df-map 8819  df-topgen 17386  df-top 22388  df-topon 22405  df-bases 22441  df-cn 22723  df-tx 23058
This theorem is referenced by:  txcn  23122
  Copyright terms: Public domain W3C validator