ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  upxp GIF version

Theorem upxp 13742
Description: Universal property of the Cartesian product considered as a categorical product in the category of sets. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 27-Dec-2014.)
Hypotheses
Ref Expression
upxp.1 š‘ƒ = (1st ā†¾ (šµ Ɨ š¶))
upxp.2 š‘„ = (2nd ā†¾ (šµ Ɨ š¶))
Assertion
Ref Expression
upxp ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ āˆƒ!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Distinct variable groups:   š“,ā„Ž   šµ,ā„Ž   š¶,ā„Ž   ā„Ž,š¹   ā„Ž,šŗ   š·,ā„Ž
Allowed substitution hints:   š‘ƒ(ā„Ž)   š‘„(ā„Ž)

Proof of Theorem upxp
Dummy variables š‘„ š‘§ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 mptexg 5741 . . . 4 (š“ āˆˆ š· ā†’ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ V)
2 eueq 2908 . . . 4 ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āˆˆ V ā†” āˆƒ!ā„Ž ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
31, 2sylib 122 . . 3 (š“ āˆˆ š· ā†’ āˆƒ!ā„Ž ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
433ad2ant1 1018 . 2 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ āˆƒ!ā„Ž ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
5 ffn 5365 . . . . . . . 8 (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ā†’ ā„Ž Fn š“)
653ad2ant1 1018 . . . . . . 7 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ ā„Ž Fn š“)
76adantl 277 . . . . . 6 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ ā„Ž Fn š“)
8 ffvelcdm 5649 . . . . . . . . . . . . 13 ((š¹:š“āŸ¶šµ āˆ§ š‘„ āˆˆ š“) ā†’ (š¹ā€˜š‘„) āˆˆ šµ)
9 ffvelcdm 5649 . . . . . . . . . . . . 13 ((šŗ:š“āŸ¶š¶ āˆ§ š‘„ āˆˆ š“) ā†’ (šŗā€˜š‘„) āˆˆ š¶)
10 opelxpi 4658 . . . . . . . . . . . . 13 (((š¹ā€˜š‘„) āˆˆ šµ āˆ§ (šŗā€˜š‘„) āˆˆ š¶) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶))
118, 9, 10syl2an 289 . . . . . . . . . . . 12 (((š¹:š“āŸ¶šµ āˆ§ š‘„ āˆˆ š“) āˆ§ (šŗ:š“āŸ¶š¶ āˆ§ š‘„ āˆˆ š“)) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶))
1211anandirs 593 . . . . . . . . . . 11 (((š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘„ āˆˆ š“) ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶))
1312ralrimiva 2550 . . . . . . . . . 10 ((š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ āˆ€š‘„ āˆˆ š“ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶))
14133adant1 1015 . . . . . . . . 9 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ āˆ€š‘„ āˆˆ š“ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶))
15 eqid 2177 . . . . . . . . . 10 (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)
1615fmpt 5666 . . . . . . . . 9 (āˆ€š‘„ āˆˆ š“ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© āˆˆ (šµ Ɨ š¶) ā†” (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶))
1714, 16sylib 122 . . . . . . . 8 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶))
1817ffnd 5366 . . . . . . 7 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn š“)
1918adantr 276 . . . . . 6 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn š“)
20 xpss 4734 . . . . . . . . . . 11 (šµ Ɨ š¶) āŠ† (V Ɨ V)
21 ffvelcdm 5649 . . . . . . . . . . 11 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (šµ Ɨ š¶))
2220, 21sselid 3153 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (V Ɨ V))
23223ad2antl1 1159 . . . . . . . . 9 (((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (V Ɨ V))
2423adantll 476 . . . . . . . 8 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (V Ɨ V))
25 fveq1 5514 . . . . . . . . . . . 12 (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†’ (š¹ā€˜š‘§) = ((š‘ƒ āˆ˜ ā„Ž)ā€˜š‘§))
26 upxp.1 . . . . . . . . . . . . . 14 š‘ƒ = (1st ā†¾ (šµ Ɨ š¶))
2726coeq1i 4786 . . . . . . . . . . . . 13 (š‘ƒ āˆ˜ ā„Ž) = ((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)
2827fveq1i 5516 . . . . . . . . . . . 12 ((š‘ƒ āˆ˜ ā„Ž)ā€˜š‘§) = (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§)
2925, 28eqtrdi 2226 . . . . . . . . . . 11 (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
30293ad2ant2 1019 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
3130ad2antlr 489 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
32 simpr1 1003 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ ā„Ž:š“āŸ¶(šµ Ɨ š¶))
33 fvco3 5587 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§) = ((1st ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
3432, 33sylan 283 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§) = ((1st ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
35213ad2antl1 1159 . . . . . . . . . . 11 (((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (šµ Ɨ š¶))
3635adantll 476 . . . . . . . . . 10 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) āˆˆ (šµ Ɨ š¶))
3736fvresd 5540 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ ((1st ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)) = (1st ā€˜(ā„Žā€˜š‘§)))
3831, 34, 373eqtrrd 2215 . . . . . . . 8 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (1st ā€˜(ā„Žā€˜š‘§)) = (š¹ā€˜š‘§))
39 fveq1 5514 . . . . . . . . . . . 12 (šŗ = (š‘„ āˆ˜ ā„Ž) ā†’ (šŗā€˜š‘§) = ((š‘„ āˆ˜ ā„Ž)ā€˜š‘§))
40 upxp.2 . . . . . . . . . . . . . 14 š‘„ = (2nd ā†¾ (šµ Ɨ š¶))
4140coeq1i 4786 . . . . . . . . . . . . 13 (š‘„ āˆ˜ ā„Ž) = ((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)
4241fveq1i 5516 . . . . . . . . . . . 12 ((š‘„ āˆ˜ ā„Ž)ā€˜š‘§) = (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§)
4339, 42eqtrdi 2226 . . . . . . . . . . 11 (šŗ = (š‘„ āˆ˜ ā„Ž) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
44433ad2ant3 1020 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
4544ad2antlr 489 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§))
46 fvco3 5587 . . . . . . . . . 10 ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§) = ((2nd ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
4732, 46sylan 283 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ ā„Ž)ā€˜š‘§) = ((2nd ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)))
4836fvresd 5540 . . . . . . . . 9 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ ((2nd ā†¾ (šµ Ɨ š¶))ā€˜(ā„Žā€˜š‘§)) = (2nd ā€˜(ā„Žā€˜š‘§)))
4945, 47, 483eqtrrd 2215 . . . . . . . 8 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (2nd ā€˜(ā„Žā€˜š‘§)) = (šŗā€˜š‘§))
50 eqopi 6172 . . . . . . . 8 (((ā„Žā€˜š‘§) āˆˆ (V Ɨ V) āˆ§ ((1st ā€˜(ā„Žā€˜š‘§)) = (š¹ā€˜š‘§) āˆ§ (2nd ā€˜(ā„Žā€˜š‘§)) = (šŗā€˜š‘§))) ā†’ (ā„Žā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
5124, 38, 49, 50syl12anc 1236 . . . . . . 7 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
52 fveq2 5515 . . . . . . . . 9 (š‘„ = š‘§ ā†’ (š¹ā€˜š‘„) = (š¹ā€˜š‘§))
53 fveq2 5515 . . . . . . . . 9 (š‘„ = š‘§ ā†’ (šŗā€˜š‘„) = (šŗā€˜š‘§))
5452, 53opeq12d 3786 . . . . . . . 8 (š‘„ = š‘§ ā†’ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ© = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
55 simpr 110 . . . . . . . 8 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ š‘§ āˆˆ š“)
5651, 36eqeltrrd 2255 . . . . . . . 8 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
5715, 54, 55, 56fvmptd3 5609 . . . . . . 7 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
5851, 57eqtr4d 2213 . . . . . 6 ((((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) āˆ§ š‘§ āˆˆ š“) ā†’ (ā„Žā€˜š‘§) = ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§))
597, 19, 58eqfnfvd 5616 . . . . 5 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))) ā†’ ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
6059ex 115 . . . 4 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†’ ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
61 ffn 5365 . . . . . . . . 9 (š¹:š“āŸ¶šµ ā†’ š¹ Fn š“)
62613ad2ant2 1019 . . . . . . . 8 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ š¹ Fn š“)
63 fo1st 6157 . . . . . . . . . . 11 1st :Vā€“ontoā†’V
64 fofn 5440 . . . . . . . . . . 11 (1st :Vā€“ontoā†’V ā†’ 1st Fn V)
6563, 64ax-mp 5 . . . . . . . . . 10 1st Fn V
66 ssv 3177 . . . . . . . . . 10 (šµ Ɨ š¶) āŠ† V
67 fnssres 5329 . . . . . . . . . 10 ((1st Fn V āˆ§ (šµ Ɨ š¶) āŠ† V) ā†’ (1st ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶))
6865, 66, 67mp2an 426 . . . . . . . . 9 (1st ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶)
6917frnd 5375 . . . . . . . . 9 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ran (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (šµ Ɨ š¶))
70 fnco 5324 . . . . . . . . 9 (((1st ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶) āˆ§ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn š“ āˆ§ ran (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (šµ Ɨ š¶)) ā†’ ((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn š“)
7168, 18, 69, 70mp3an2i 1342 . . . . . . . 8 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn š“)
72 fvco3 5587 . . . . . . . . . 10 (((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
7317, 72sylan 283 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((1st ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
74 simpr 110 . . . . . . . . . . 11 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ š‘§ āˆˆ š“)
75 simpl2 1001 . . . . . . . . . . . . 13 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ š¹:š“āŸ¶šµ)
7675, 74ffvelcdmd 5652 . . . . . . . . . . . 12 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (š¹ā€˜š‘§) āˆˆ šµ)
77 simpl3 1002 . . . . . . . . . . . . 13 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ šŗ:š“āŸ¶š¶)
7877, 74ffvelcdmd 5652 . . . . . . . . . . . 12 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (šŗā€˜š‘§) āˆˆ š¶)
7976, 78opelxpd 4659 . . . . . . . . . . 11 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
8015, 54, 74, 79fvmptd3 5609 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§) = āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©)
8180fveq2d 5519 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((1st ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((1st ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
82 ffvelcdm 5649 . . . . . . . . . . . . . 14 ((š¹:š“āŸ¶šµ āˆ§ š‘§ āˆˆ š“) ā†’ (š¹ā€˜š‘§) āˆˆ šµ)
83 ffvelcdm 5649 . . . . . . . . . . . . . 14 ((šŗ:š“āŸ¶š¶ āˆ§ š‘§ āˆˆ š“) ā†’ (šŗā€˜š‘§) āˆˆ š¶)
84 opelxpi 4658 . . . . . . . . . . . . . 14 (((š¹ā€˜š‘§) āˆˆ šµ āˆ§ (šŗā€˜š‘§) āˆˆ š¶) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
8582, 83, 84syl2an 289 . . . . . . . . . . . . 13 (((š¹:š“āŸ¶šµ āˆ§ š‘§ āˆˆ š“) āˆ§ (šŗ:š“āŸ¶š¶ āˆ§ š‘§ āˆˆ š“)) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
8685anandirs 593 . . . . . . . . . . . 12 (((š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
87863adantl1 1153 . . . . . . . . . . 11 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ© āˆˆ (šµ Ɨ š¶))
8887fvresd 5540 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((1st ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
89 op1stg 6150 . . . . . . . . . . 11 (((š¹ā€˜š‘§) āˆˆ šµ āˆ§ (šŗā€˜š‘§) āˆˆ š¶) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
9076, 78, 89syl2anc 411 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (1st ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
9188, 90eqtrd 2210 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((1st ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (š¹ā€˜š‘§))
9273, 81, 913eqtrrd 2215 . . . . . . . 8 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (š¹ā€˜š‘§) = (((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
9362, 71, 92eqfnfvd 5616 . . . . . . 7 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ š¹ = ((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
9426coeq1i 4786 . . . . . . 7 (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((1st ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
9593, 94eqtr4di 2228 . . . . . 6 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
96 ffn 5365 . . . . . . . . 9 (šŗ:š“āŸ¶š¶ ā†’ šŗ Fn š“)
97963ad2ant3 1020 . . . . . . . 8 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ šŗ Fn š“)
98 fo2nd 6158 . . . . . . . . . . 11 2nd :Vā€“ontoā†’V
99 fofn 5440 . . . . . . . . . . 11 (2nd :Vā€“ontoā†’V ā†’ 2nd Fn V)
10098, 99ax-mp 5 . . . . . . . . . 10 2nd Fn V
101 fnssres 5329 . . . . . . . . . 10 ((2nd Fn V āˆ§ (šµ Ɨ š¶) āŠ† V) ā†’ (2nd ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶))
102100, 66, 101mp2an 426 . . . . . . . . 9 (2nd ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶)
103 fnco 5324 . . . . . . . . 9 (((2nd ā†¾ (šµ Ɨ š¶)) Fn (šµ Ɨ š¶) āˆ§ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) Fn š“ āˆ§ ran (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) āŠ† (šµ Ɨ š¶)) ā†’ ((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn š“)
104102, 18, 69, 103mp3an2i 1342 . . . . . . . 8 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) Fn š“)
105 fvco3 5587 . . . . . . . . . 10 (((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
10617, 105sylan 283 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§) = ((2nd ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)))
10780fveq2d 5519 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((2nd ā†¾ (šµ Ɨ š¶))ā€˜((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)ā€˜š‘§)) = ((2nd ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
10887fvresd 5540 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((2nd ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©))
109 op2ndg 6151 . . . . . . . . . . 11 (((š¹ā€˜š‘§) āˆˆ šµ āˆ§ (šŗā€˜š‘§) āˆˆ š¶) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
11076, 78, 109syl2anc 411 . . . . . . . . . 10 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (2nd ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
111108, 110eqtrd 2210 . . . . . . . . 9 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ ((2nd ā†¾ (šµ Ɨ š¶))ā€˜āŸØ(š¹ā€˜š‘§), (šŗā€˜š‘§)āŸ©) = (šŗā€˜š‘§))
112106, 107, 1113eqtrrd 2215 . . . . . . . 8 (((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) āˆ§ š‘§ āˆˆ š“) ā†’ (šŗā€˜š‘§) = (((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))ā€˜š‘§))
11397, 104, 112eqfnfvd 5616 . . . . . . 7 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ šŗ = ((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
11440coeq1i 4786 . . . . . . 7 (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) = ((2nd ā†¾ (šµ Ɨ š¶)) āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))
115113, 114eqtr4di 2228 . . . . . 6 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
11617, 95, 1153jca 1177 . . . . 5 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
117 feq1 5348 . . . . . 6 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) ā†” (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶)))
118 coeq2 4785 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘ƒ āˆ˜ ā„Ž) = (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
119118eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š¹ = (š‘ƒ āˆ˜ ā„Ž) ā†” š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
120 coeq2 4785 . . . . . . 7 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (š‘„ āˆ˜ ā„Ž) = (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
121120eqeq2d 2189 . . . . . 6 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (šŗ = (š‘„ āˆ˜ ā„Ž) ā†” šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©))))
122117, 119, 1213anbi123d 1312 . . . . 5 (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” ((š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©):š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)) āˆ§ šŗ = (š‘„ āˆ˜ (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))))
123116, 122syl5ibrcom 157 . . . 4 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ (ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©) ā†’ (ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž))))
12460, 123impbid 129 . . 3 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ ((ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
125124eubidv 2034 . 2 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ (āˆƒ!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)) ā†” āˆƒ!ā„Ž ā„Ž = (š‘„ āˆˆ š“ ā†¦ āŸØ(š¹ā€˜š‘„), (šŗā€˜š‘„)āŸ©)))
1264, 125mpbird 167 1 ((š“ āˆˆ š· āˆ§ š¹:š“āŸ¶šµ āˆ§ šŗ:š“āŸ¶š¶) ā†’ āˆƒ!ā„Ž(ā„Ž:š“āŸ¶(šµ Ɨ š¶) āˆ§ š¹ = (š‘ƒ āˆ˜ ā„Ž) āˆ§ šŗ = (š‘„ āˆ˜ ā„Ž)))
Colors of variables: wff set class
Syntax hints:   ā†’ wi 4   āˆ§ wa 104   āˆ§ w3a 978   = wceq 1353  āˆƒ!weu 2026   āˆˆ wcel 2148  āˆ€wral 2455  Vcvv 2737   āŠ† wss 3129  āŸØcop 3595   ā†¦ cmpt 4064   Ɨ cxp 4624  ran crn 4627   ā†¾ cres 4628   āˆ˜ ccom 4630   Fn wfn 5211  āŸ¶wf 5212  ā€“ontoā†’wfo 5214  ā€˜cfv 5216  1st c1st 6138  2nd c2nd 6139
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-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
This theorem depends on definitions:  df-bi 117  df-3an 980  df-tru 1356  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-ral 2460  df-rex 2461  df-reu 2462  df-rab 2464  df-v 2739  df-sbc 2963  df-csb 3058  df-un 3133  df-in 3135  df-ss 3142  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-1st 6140  df-2nd 6141
This theorem is referenced by:  uptx  13744  txcn  13745
  Copyright terms: Public domain W3C validator