ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uptx GIF version
Theorem uptx 13777
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 2177 . . . . 5 āˆŖ š‘ˆ = āˆŖ š‘ˆ
2 eqid 2177 . . . . 5 (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)
31, 2txcnmpt 13776 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn (š‘… Ɨt š‘†)))
4 uptx.1 . . . . 5 š‘‡ = (š‘… Ɨt š‘†)
54oveq2i 5886 . . . 4 (š‘ˆ Cn š‘‡) = (š‘ˆ Cn (š‘… Ɨt š‘†))
63, 5eleqtrrdi 2271 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡))
7 uptx.2 . . . . . 6 š‘‹ = āˆŖ š‘…
81, 7cnf 13707 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
9 uptx.3 . . . . . 6 š‘Œ = āˆŖ š‘†
101, 9cnf 13707 . . . . 5 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
11 ffn 5366 . . . . . . . 8 (š¹:āˆŖ š‘ˆāŸ¶š‘‹ ā†’ š¹ Fn āˆŖ š‘ˆ)
1211adantr 276 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ Fn āˆŖ š‘ˆ)
13 fo1st 6158 . . . . . . . . . 10 1st :Vā€“ontoā†’V
14 fofn 5441 . . . . . . . . . 10 (1st :Vā€“ontoā†’V ā†’ 1st Fn V)
1513, 14ax-mp 5 . . . . . . . . 9 1st Fn V
16 ssv 3178 . . . . . . . . 9 (š‘‹ Ɨ š‘Œ) āŠ† V
17 fnssres 5330 . . . . . . . . 9 ((1st Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
1815, 16, 17mp2an 426 . . . . . . . 8 (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
19 ffvelcdm 5650 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘„) āˆˆ š‘‹)
20 ffvelcdm 5650 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘„) āˆˆ š‘Œ)
21 opelxpi 4659 . . . . . . . . . . . 12 (((š¹ā€˜š‘„) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘„) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2219, 20, 21syl2an 289 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2322anandirs 593 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2423fmpttd 5672 . . . . . . . . 9 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ))
2524ffnd 5367 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2624frnd 5376 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ))
27 fnco 5325 . . . . . . . 8 (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
2818, 25, 26, 27mp3an2i 1342 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
29 fvco3 5588 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
3024, 29sylan 283 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
31 fveq2 5516 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
32 fveq2 5516 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ (šŗā€˜š‘„) = (šŗā€˜š‘§))
3331, 32opeq12d 3787 . . . . . . . . . 10 (š‘„ = š‘§ ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
34 simpr 110 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ š‘§ āˆˆ āˆŖ š‘ˆ)
35 simpll 527 . . . . . . . . . . . 12 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
3635, 34ffvelcdmd 5653 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
37 simplr 528 . . . . . . . . . . . 12 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
3837, 34ffvelcdmd 5653 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
3936, 38opelxpd 4660 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
402, 33, 34, 39fvmptd3 5610 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
4140fveq2d 5520 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
42 ffvelcdm 5650 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
43 ffvelcdm 5650 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
44 opelxpi 4659 . . . . . . . . . . . 12 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4542, 43, 44syl2an 289 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4645anandirs 593 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4746fvresd 5541 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
48 op1stg 6151 . . . . . . . . . 10 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
4936, 38, 48syl2anc 411 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
5047, 49eqtrd 2210 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
5130, 41, 503eqtrrd 2215 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
5212, 28, 51eqfnfvd 5617 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
53 uptx.5 . . . . . . . 8 š‘ƒ = (1st ā†¾ š‘)
54 uptx.4 . . . . . . . . 9 š‘ = (š‘‹ Ɨ š‘Œ)
5554reseq2i 4905 . . . . . . . 8 (1st ā†¾ š‘) = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5653, 55eqtri 2198 . . . . . . 7 š‘ƒ = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5756coeq1i 4787 . . . . . 6 (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
5852, 57eqtr4di 2228 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
598, 10, 58syl2an 289 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
60 ffn 5366 . . . . . . . 8 (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ ā†’ šŗ Fn āˆŖ š‘ˆ)
6160adantl 277 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ Fn āˆŖ š‘ˆ)
62 fo2nd 6159 . . . . . . . . . 10 2nd :Vā€“ontoā†’V
63 fofn 5441 . . . . . . . . . 10 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
6462, 63ax-mp 5 . . . . . . . . 9 2nd Fn V
65 fnssres 5330 . . . . . . . . 9 ((2nd Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
6664, 16, 65mp2an 426 . . . . . . . 8 (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
67 fnco 5325 . . . . . . . 8 (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
6866, 25, 26, 67mp3an2i 1342 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
69 fvco3 5588 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
7024, 69sylan 283 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
7140fveq2d 5520 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7246fvresd 5541 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
73 op2ndg 6152 . . . . . . . . . 10 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7436, 38, 73syl2anc 411 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7572, 74eqtrd 2210 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7670, 71, 753eqtrrd 2215 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
7761, 68, 76eqfnfvd 5617 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
78 uptx.6 . . . . . . . 8 š‘„ = (2nd ā†¾ š‘)
7954reseq2i 4905 . . . . . . . 8 (2nd ā†¾ š‘) = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
8078, 79eqtri 2198 . . . . . . 7 š‘„ = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
8180coeq1i 4787 . . . . . 6 (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
8277, 81eqtr4di 2228 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
838, 10, 82syl2an 289 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
846, 59, 83jca32 310 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
85 eleq1 2240 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†” (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡)))
86 coeq2 4786 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘ƒ āˆ˜ ā„Ž) = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8786eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†” š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
88 coeq2 4786 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘„ āˆ˜ ā„Ž) = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8988eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (šŗ = (š‘„ āˆ˜ ā„Ž) ā†” šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
9087, 89anbi12d 473 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
9185, 90anbi12d 473 . . . 4 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))))
9291spcegv 2826 . . 3 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) ā†’ (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
936, 84, 92sylc 62 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
94 eqid 2177 . . . . . . . 8 āˆŖ š‘‡ = āˆŖ š‘‡
951, 94cnf 13707 . . . . . . 7 (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡)
96 cntop2 13705 . . . . . . . . 9 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘… āˆˆ Top)
97 cntop2 13705 . . . . . . . . 9 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ š‘† āˆˆ Top)
984unieqi 3820 . . . . . . . . . 10 āˆŖ š‘‡ = āˆŖ (š‘… Ɨt š‘†)
997, 9txuni 13766 . . . . . . . . . 10 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ (š‘‹ Ɨ š‘Œ) = āˆŖ (š‘… Ɨt š‘†))
10098, 99eqtr4id 2229 . . . . . . . . 9 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
10196, 97, 100syl2an 289 . . . . . . . 8 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
102101feq3d 5355 . . . . . . 7 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡ ā†” ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
10395, 102imbitrid 154 . . . . . 6 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ)))
104103anim1d 336 . . . . 5 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
105 3anass 982 . . . . 5 ((ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
106104, 105imbitrrdi 162 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
107106alrimiv 1874 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
108 cntop1 13704 . . . . . 6 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘ˆ āˆˆ Top)
109 uniexg 4440 . . . . . 6 (š‘ˆ āˆˆ Top ā†’ āˆŖ š‘ˆ āˆˆ V)
110108, 109syl 14 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ āˆŖ š‘ˆ āˆˆ V)
11156, 80upxp 13775 . . . . 5 ((āˆŖ š‘ˆ āˆˆ V āˆ§ š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
112110, 8, 10, 111syl2an3an 1298 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
113 eumo 2058 . . . 4 (āˆƒ!ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
114112, 113syl 14 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
115 moim 2090 . . 3 (āˆ€ā„Ž((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (āˆƒ*ā„Ž(ā„Ž:āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
116107, 114, 115sylc 62 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
117 df-reu 2462 . . 3 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
118 eu5 2073 . . 3 (āˆƒ!ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
119117, 118bitri 184 . 2 (āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ āˆƒ*ā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
12093, 116, 119sylanbrc 417 1 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒ!ā„Ž āˆˆ (š‘ˆ Cn š‘‡)(š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Colors of variables: wff set class
Syntax hints:   ā†’ wi 4   āˆ§ wa 104   āˆ§ w3a 978  āˆ€wal 1351   = wceq 1353  āˆƒwex 1492  āˆƒ!weu 2026  āˆƒ*wmo 2027   āˆˆ wcel 2148  āˆƒ!wreu 2457  Vcvv 2738   āŠ† wss 3130  āŸØcop 3596  āˆŖ cuni 3810   ā†¦ cmpt 4065   Ɨ cxp 4625  ran crn 4628   ā†¾ cres 4629   āˆ˜ ccom 4631   Fn wfn 5212  āŸ¶wf 5213  ā€“ontoā†’wfo 5215  ā€˜cfv 5217  (class class class)co 5875  1st c1st 6139  2nd c2nd 6140  Topctop 13500   Cn ccn 13688   Ɨt ctx 13755
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 614  ax-in2 615  ax-io 709  ax-5 1447  ax-7 1448  ax-gen 1449  ax-ie1 1493  ax-ie2 1494  ax-8 1504  ax-10 1505  ax-11 1506  ax-i12 1507  ax-bndl 1509  ax-4 1510  ax-17 1526  ax-i9 1530  ax-ial 1534  ax-i5r 1535  ax-13 2150  ax-14 2151  ax-ext 2159  ax-coll 4119  ax-sep 4122  ax-pow 4175  ax-pr 4210  ax-un 4434  ax-setind 4537
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  df-fal 1359  df-nf 1461  df-sb 1763  df-eu 2029  df-mo 2030  df-clab 2164  df-cleq 2170  df-clel 2173  df-nfc 2308  df-ne 2348  df-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2740  df-sbc 2964  df-csb 3059  df-dif 3132  df-un 3134  df-in 3136  df-ss 3143  df-nul 3424  df-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-xp 4633  df-rel 4634  df-cnv 4635  df-co 4636  df-dm 4637  df-rn 4638  df-res 4639  df-ima 4640  df-iota 5179  df-fun 5219  df-fn 5220  df-f 5221  df-f1 5222  df-fo 5223  df-f1o 5224  df-fv 5225  df-ov 5878  df-oprab 5879  df-mpo 5880  df-1st 6141  df-2nd 6142  df-map 6650  df-topgen 12709  df-top 13501  df-topon 13514  df-bases 13546  df-cn 13691  df-tx 13756
This theorem is referenced by:  txcn  13778
  Copyright terms: Public domain W3C validator