ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  uptx GIF version
Theorem uptx 13744
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 13743 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn (š‘… Ɨt š‘†)))
4 uptx.1 . . . . 5 š‘‡ = (š‘… Ɨt š‘†)
54oveq2i 5885 . . . 4 (š‘ˆ Cn š‘‡) = (š‘ˆ Cn (š‘… Ɨt š‘†))
63, 5eleqtrrdi 2271 . . 3 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡))
7 uptx.2 . . . . . 6 š‘‹ = āˆŖ š‘…
81, 7cnf 13674 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
9 uptx.3 . . . . . 6 š‘Œ = āˆŖ š‘†
101, 9cnf 13674 . . . . 5 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
11 ffn 5365 . . . . . . . 8 (š¹:āˆŖ š‘ˆāŸ¶š‘‹ ā†’ š¹ Fn āˆŖ š‘ˆ)
1211adantr 276 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ Fn āˆŖ š‘ˆ)
13 fo1st 6157 . . . . . . . . . 10 1st :Vā€“ontoā†’V
14 fofn 5440 . . . . . . . . . 10 (1st :Vā€“ontoā†’V ā†’ 1st Fn V)
1513, 14ax-mp 5 . . . . . . . . 9 1st Fn V
16 ssv 3177 . . . . . . . . 9 (š‘‹ Ɨ š‘Œ) āŠ† V
17 fnssres 5329 . . . . . . . . 9 ((1st Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
1815, 16, 17mp2an 426 . . . . . . . 8 (1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
19 ffvelcdm 5649 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘„) āˆˆ š‘‹)
20 ffvelcdm 5649 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘„) āˆˆ š‘Œ)
21 opelxpi 4658 . . . . . . . . . . . 12 (((š¹ā€˜š‘„) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘„) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2219, 20, 21syl2an 289 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2322anandirs 593 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘„ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
2423fmpttd 5671 . . . . . . . . 9 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ))
2524ffnd 5366 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ)
2624frnd 5375 . . . . . . . 8 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ))
27 fnco 5324 . . . . . . . 8 (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
2818, 25, 26, 27mp3an2i 1342 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
29 fvco3 5587 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
3024, 29sylan 283 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
31 fveq2 5515 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
32 fveq2 5515 . . . . . . . . . . 11 (š‘„ = š‘§ ā†’ (šŗā€˜š‘„) = (šŗā€˜š‘§))
3331, 32opeq12d 3786 . . . . . . . . . 10 (š‘„ = š‘§ ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
34 simpr 110 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ š‘§ āˆˆ āˆŖ š‘ˆ)
35 simpll 527 . . . . . . . . . . . 12 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ š¹:āˆŖ š‘ˆāŸ¶š‘‹)
3635, 34ffvelcdmd 5652 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
37 simplr 528 . . . . . . . . . . . 12 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ)
3837, 34ffvelcdmd 5652 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
3936, 38opelxpd 4659 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
402, 33, 34, 39fvmptd3 5609 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
4140fveq2d 5519 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
42 ffvelcdm 5649 . . . . . . . . . . . 12 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) āˆˆ š‘‹)
43 ffvelcdm 5649 . . . . . . . . . . . 12 ((šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) āˆˆ š‘Œ)
44 opelxpi 4658 . . . . . . . . . . . 12 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4542, 43, 44syl2an 289 . . . . . . . . . . 11 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) āˆ§ (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ)) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4645anandirs 593 . . . . . . . . . 10 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (š‘‹ Ɨ š‘Œ))
4746fvresd 5540 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
48 op1stg 6150 . . . . . . . . . 10 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
4936, 38, 48syl2anc 411 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
5047, 49eqtrd 2210 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((1st ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
5130, 41, 503eqtrrd 2215 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
5212, 28, 51eqfnfvd 5616 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
53 uptx.5 . . . . . . . 8 š‘ƒ = (1st ā†¾ š‘)
54 uptx.4 . . . . . . . . 9 š‘ = (š‘‹ Ɨ š‘Œ)
5554reseq2i 4904 . . . . . . . 8 (1st ā†¾ š‘) = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5653, 55eqtri 2198 . . . . . . 7 š‘ƒ = (1st ā†¾ (š‘‹ Ɨ š‘Œ))
5756coeq1i 4786 . . . . . 6 (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((1st ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
5852, 57eqtr4di 2228 . . . . 5 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
598, 10, 58syl2an 289 . . . 4 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
60 ffn 5365 . . . . . . . 8 (šŗ:āˆŖ š‘ˆāŸ¶š‘Œ ā†’ šŗ Fn āˆŖ š‘ˆ)
6160adantl 277 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ Fn āˆŖ š‘ˆ)
62 fo2nd 6158 . . . . . . . . . 10 2nd :Vā€“ontoā†’V
63 fofn 5440 . . . . . . . . . 10 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
6462, 63ax-mp 5 . . . . . . . . 9 2nd Fn V
65 fnssres 5329 . . . . . . . . 9 ((2nd Fn V āˆ§ (š‘‹ Ɨ š‘Œ) āŠ† V) ā†’ (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ))
6664, 16, 65mp2an 426 . . . . . . . 8 (2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ)
67 fnco 5324 . . . . . . . 8 (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) Fn (š‘‹ Ɨ š‘Œ) āˆ§ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn āˆŖ š‘ˆ āˆ§ ran (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (š‘‹ Ɨ š‘Œ)) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
6866, 25, 26, 67mp3an2i 1342 . . . . . . 7 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn āˆŖ š‘ˆ)
69 fvco3 5587 . . . . . . . . 9 (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):āˆŖ š‘ˆāŸ¶(š‘‹ Ɨ š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
7024, 69sylan 283 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
7140fveq2d 5519 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
7246fvresd 5540 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
73 op2ndg 6151 . . . . . . . . . 10 (((š¹ā€˜š‘§) āˆˆ š‘‹ āˆ§ (šŗā€˜š‘§) āˆˆ š‘Œ) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7436, 38, 73syl2anc 411 . . . . . . . . 9 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7572, 74eqtrd 2210 . . . . . . . 8 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ ((2nd ā†¾ (š‘‹ Ɨ š‘Œ))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
7670, 71, 753eqtrrd 2215 . . . . . . 7 (((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) āˆ§ š‘§ āˆˆ āˆŖ š‘ˆ) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
7761, 68, 76eqfnfvd 5616 . . . . . 6 ((š¹:āˆŖ š‘ˆāŸ¶š‘‹ āˆ§ šŗ:āˆŖ š‘ˆāŸ¶š‘Œ) ā†’ šŗ = ((2nd ā†¾ (š‘‹ Ɨ š‘Œ)) āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
78 uptx.6 . . . . . . . 8 š‘„ = (2nd ā†¾ š‘)
7954reseq2i 4904 . . . . . . . 8 (2nd ā†¾ š‘) = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
8078, 79eqtri 2198 . . . . . . 7 š‘„ = (2nd ā†¾ (š‘‹ Ɨ š‘Œ))
8180coeq1i 4786 . . . . . 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 4785 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘ƒ āˆ˜ ā„Ž) = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8786eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†” š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
88 coeq2 4785 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘„ āˆ˜ ā„Ž) = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
8988eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (šŗ = (š‘„ āˆ˜ ā„Ž) ā†” šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
9087, 89anbi12d 473 . . . . 5 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
9185, 90anbi12d 473 . . . 4 (ā„Ž = (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†” ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))))
9291spcegv 2825 . . 3 ((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) ā†’ (((š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ āˆŖ š‘ˆ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))))
936, 84, 92sylc 62 . 2 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆƒā„Ž(ā„Ž āˆˆ (š‘ˆ Cn š‘‡) āˆ§ (š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
94 eqid 2177 . . . . . . . 8 āˆŖ š‘‡ = āˆŖ š‘‡
951, 94cnf 13674 . . . . . . 7 (ā„Ž āˆˆ (š‘ˆ Cn š‘‡) ā†’ ā„Ž:āˆŖ š‘ˆāŸ¶āˆŖ š‘‡)
96 cntop2 13672 . . . . . . . . 9 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘… āˆˆ Top)
97 cntop2 13672 . . . . . . . . 9 (šŗ āˆˆ (š‘ˆ Cn š‘†) ā†’ š‘† āˆˆ Top)
984unieqi 3819 . . . . . . . . . 10 āˆŖ š‘‡ = āˆŖ (š‘… Ɨt š‘†)
997, 9txuni 13733 . . . . . . . . . 10 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ (š‘‹ Ɨ š‘Œ) = āˆŖ (š‘… Ɨt š‘†))
10098, 99eqtr4id 2229 . . . . . . . . 9 ((š‘… āˆˆ Top āˆ§ š‘† āˆˆ Top) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
10196, 97, 100syl2an 289 . . . . . . . 8 ((š¹ āˆˆ (š‘ˆ Cn š‘…) āˆ§ šŗ āˆˆ (š‘ˆ Cn š‘†)) ā†’ āˆŖ š‘‡ = (š‘‹ Ɨ š‘Œ))
102101feq3d 5354 . . . . . . 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 13671 . . . . . 6 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ š‘ˆ āˆˆ Top)
109 uniexg 4439 . . . . . 6 (š‘ˆ āˆˆ Top ā†’ āˆŖ š‘ˆ āˆˆ V)
110108, 109syl 14 . . . . 5 (š¹ āˆˆ (š‘ˆ Cn š‘…) ā†’ āˆŖ š‘ˆ āˆˆ V)
11156, 80upxp 13742 . . . . 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 2737   āŠ† wss 3129  āŸØcop 3595  āˆŖ cuni 3809   ā†¦ cmpt 4064   Ɨ cxp 4624  ran crn 4627   ā†¾ cres 4628   āˆ˜ ccom 4630   Fn wfn 5211  āŸ¶wf 5212  ā€“ontoā†’wfo 5214  ā€˜cfv 5216  (class class class)co 5874  1st c1st 6138  2nd c2nd 6139  Topctop 13467   Cn ccn 13655   Ɨt ctx 13722
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 4118  ax-sep 4121  ax-pow 4174  ax-pr 4209  ax-un 4433  ax-setind 4536
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 2739  df-sbc 2963  df-csb 3058  df-dif 3131  df-un 3133  df-in 3135  df-ss 3142  df-nul 3423  df-pw 3577  df-sn 3598  df-pr 3599  df-op 3601  df-uni 3810  df-iun 3888  df-br 4004  df-opab 4065  df-mpt 4066  df-id 4293  df-xp 4632  df-rel 4633  df-cnv 4634  df-co 4635  df-dm 4636  df-rn 4637  df-res 4638  df-ima 4639  df-iota 5178  df-fun 5218  df-fn 5219  df-f 5220  df-f1 5221  df-fo 5222  df-f1o 5223  df-fv 5224  df-ov 5877  df-oprab 5878  df-mpo 5879  df-1st 6140  df-2nd 6141  df-map 6649  df-topgen 12708  df-top 13468  df-topon 13481  df-bases 13513  df-cn 13658  df-tx 13723
This theorem is referenced by:  txcn  13745
  Copyright terms: Public domain W3C validator