MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  poxp Structured version   Visualization version   GIF version

Theorem poxp 8118
Description: A lexicographical ordering of two posets. (Contributed by Scott Fenton, 16-Mar-2011.) (Revised by Mario Carneiro, 7-Mar-2013.)
Hypothesis
Ref Expression
poxp.1 š‘‡ = {āŸØš‘„, š‘¦āŸ© āˆ£ ((š‘„ āˆˆ (š“ Ɨ šµ) āˆ§ š‘¦ āˆˆ (š“ Ɨ šµ)) āˆ§ ((1st ā€˜š‘„)š‘…(1st ā€˜š‘¦) āˆØ ((1st ā€˜š‘„) = (1st ā€˜š‘¦) āˆ§ (2nd ā€˜š‘„)š‘†(2nd ā€˜š‘¦))))}
Assertion
Ref Expression
poxp ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ š‘‡ Po (š“ Ɨ šµ))
Distinct variable groups:   š‘„,š“,š‘¦   š‘„,šµ,š‘¦   š‘„,š‘…,š‘¦   š‘„,š‘†,š‘¦
Allowed substitution hints:   š‘‡(š‘„,š‘¦)

Proof of Theorem poxp
Dummy variables š‘Ž š‘ š‘ š‘‘ š‘’ š‘“ š‘” š‘¢ š‘£ are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 elxp 5700 . . . . . . . 8 (š‘” āˆˆ (š“ Ɨ šµ) ā†” āˆƒš‘Žāˆƒš‘(š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)))
2 elxp 5700 . . . . . . . 8 (š‘¢ āˆˆ (š“ Ɨ šµ) ā†” āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)))
3 elxp 5700 . . . . . . . 8 (š‘£ āˆˆ (š“ Ɨ šµ) ā†” āˆƒš‘’āˆƒš‘“(š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)))
4 3an6 1444 . . . . . . . . . . . . . . . . 17 (((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†” ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))))
5 poirr 5601 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((š‘… Po š“ āˆ§ š‘Ž āˆˆ š“) ā†’ Ā¬ š‘Žš‘…š‘Ž)
65ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (š‘… Po š“ ā†’ (š‘Ž āˆˆ š“ ā†’ Ā¬ š‘Žš‘…š‘Ž))
7 poirr 5601 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((š‘† Po šµ āˆ§ š‘ āˆˆ šµ) ā†’ Ā¬ š‘š‘†š‘)
87intnand 487 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ((š‘† Po šµ āˆ§ š‘ āˆˆ šµ) ā†’ Ā¬ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))
98ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (š‘† Po šµ ā†’ (š‘ āˆˆ šµ ā†’ Ā¬ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘)))
106, 9im2anan9 618 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) ā†’ (Ā¬ š‘Žš‘…š‘Ž āˆ§ Ā¬ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
11 ioran 980 . . . . . . . . . . . . . . . . . . . . . . . . 25 (Ā¬ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘)) ā†” (Ā¬ š‘Žš‘…š‘Ž āˆ§ Ā¬ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘)))
1210, 11imbitrrdi 251 . . . . . . . . . . . . . . . . . . . . . . . 24 ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) ā†’ Ā¬ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
1312imp 405 . . . . . . . . . . . . . . . . . . . . . . 23 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ Ā¬ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘)))
1413intnand 487 . . . . . . . . . . . . . . . . . . . . . 22 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
15143ad2antr1 1186 . . . . . . . . . . . . . . . . . . . . 21 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
16 an4 652 . . . . . . . . . . . . . . . . . . . . . 22 (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†” ((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ ((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ))) āˆ§ ((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))))
17 3an6 1444 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†” ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)))
18 potr 5602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) ā†’ ((š‘Žš‘…š‘ āˆ§ š‘š‘…š‘’) ā†’ š‘Žš‘…š‘’))
19183impia 1115 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘Žš‘…š‘ āˆ§ š‘š‘…š‘’)) ā†’ š‘Žš‘…š‘’)
2019orcd 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 ((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘Žš‘…š‘ āˆ§ š‘š‘…š‘’)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))
21203expia 1119 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 ((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) ā†’ ((š‘Žš‘…š‘ āˆ§ š‘š‘…š‘’) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
2221expdimp 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) āˆ§ š‘Žš‘…š‘) ā†’ (š‘š‘…š‘’ ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
23 breq2 5153 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (š‘ = š‘’ ā†’ (š‘Žš‘…š‘ ā†” š‘Žš‘…š‘’))
2423biimpa 475 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 ((š‘ = š‘’ āˆ§ š‘Žš‘…š‘) ā†’ š‘Žš‘…š‘’)
2524orcd 869 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 ((š‘ = š‘’ āˆ§ š‘Žš‘…š‘) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))
2625expcom 412 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (š‘Žš‘…š‘ ā†’ (š‘ = š‘’ ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
2726adantrd 490 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (š‘Žš‘…š‘ ā†’ ((š‘ = š‘’ āˆ§ š‘‘š‘†š‘“) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
2827adantl 480 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) āˆ§ š‘Žš‘…š‘) ā†’ ((š‘ = š‘’ āˆ§ š‘‘š‘†š‘“) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
2922, 28jaod 855 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 (((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) āˆ§ š‘Žš‘…š‘) ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
3029ex 411 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) ā†’ (š‘Žš‘…š‘ ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
31 potr 5602 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 ((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘š‘†š‘‘ āˆ§ š‘‘š‘†š‘“) ā†’ š‘š‘†š‘“))
3231expdimp 451 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ š‘š‘†š‘‘) ā†’ (š‘‘š‘†š‘“ ā†’ š‘š‘†š‘“))
3332anim2d 610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ š‘š‘†š‘‘) ā†’ ((š‘ = š‘’ āˆ§ š‘‘š‘†š‘“) ā†’ (š‘ = š‘’ āˆ§ š‘š‘†š‘“)))
3433orim2d 963 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ š‘š‘†š‘‘) ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘š‘†š‘“))))
35 breq1 5152 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (š‘Ž = š‘ ā†’ (š‘Žš‘…š‘’ ā†” š‘š‘…š‘’))
36 equequ1 2026 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 (š‘Ž = š‘ ā†’ (š‘Ž = š‘’ ā†” š‘ = š‘’))
3736anbi1d 628 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 (š‘Ž = š‘ ā†’ ((š‘Ž = š‘’ āˆ§ š‘š‘†š‘“) ā†” (š‘ = š‘’ āˆ§ š‘š‘†š‘“)))
3835, 37orbi12d 915 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 (š‘Ž = š‘ ā†’ ((š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)) ā†” (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘š‘†š‘“))))
3938imbi2d 339 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 (š‘Ž = š‘ ā†’ (((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))) ā†” ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘š‘†š‘“)))))
4034, 39imbitrrid 245 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 (š‘Ž = š‘ ā†’ (((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ š‘š‘†š‘‘) ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
4140expd 414 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 (š‘Ž = š‘ ā†’ ((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) ā†’ (š‘š‘†š‘‘ ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))))
4241com12 32 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 ((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) ā†’ (š‘Ž = š‘ ā†’ (š‘š‘†š‘‘ ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))))
4342impd 409 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ((š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘Ž = š‘ āˆ§ š‘š‘†š‘‘) ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
4430, 43jaao 951 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) āˆ§ (š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ))) ā†’ ((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) ā†’ ((š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
4544impd 409 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((š‘… Po š“ āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“)) āˆ§ (š‘† Po šµ āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“))) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
4645an4s 656 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“))) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
4717, 46sylan2b 592 . . . . . . . . . . . . . . . . . . . . . . . 24 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“))) ā†’ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
48 an4 652 . . . . . . . . . . . . . . . . . . . . . . . . . . 27 (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†” ((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)))
4948biimpi 215 . . . . . . . . . . . . . . . . . . . . . . . . . 26 (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)))
50493adant2 1129 . . . . . . . . . . . . . . . . . . . . . . . . 25 (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)))
5150adantl 480 . . . . . . . . . . . . . . . . . . . . . . . 24 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ ((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)))
5247, 51jctild 524 . . . . . . . . . . . . . . . . . . . . . . 23 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
5352adantld 489 . . . . . . . . . . . . . . . . . . . . . 22 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ ((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ))) āˆ§ ((š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
5416, 53biimtrid 241 . . . . . . . . . . . . . . . . . . . . 21 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
5515, 54jca 510 . . . . . . . . . . . . . . . . . . . 20 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))) āˆ§ (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))))
56 breq12 5154 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘” = āŸØš‘Ž, š‘āŸ©) ā†’ (š‘”š‘‡š‘” ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ©))
5756anidms 565 . . . . . . . . . . . . . . . . . . . . . . . 24 (š‘” = āŸØš‘Ž, š‘āŸ© ā†’ (š‘”š‘‡š‘” ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ©))
5857notbid 317 . . . . . . . . . . . . . . . . . . . . . . 23 (š‘” = āŸØš‘Ž, š‘āŸ© ā†’ (Ā¬ š‘”š‘‡š‘” ā†” Ā¬ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ©))
59583ad2ant1 1131 . . . . . . . . . . . . . . . . . . . . . 22 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (Ā¬ š‘”š‘‡š‘” ā†” Ā¬ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ©))
60 breq12 5154 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ©) ā†’ (š‘”š‘‡š‘¢ ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ©))
61603adant3 1130 . . . . . . . . . . . . . . . . . . . . . . . 24 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (š‘”š‘‡š‘¢ ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ©))
62 breq12 5154 . . . . . . . . . . . . . . . . . . . . . . . . 25 ((š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (š‘¢š‘‡š‘£ ā†” āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©))
63623adant1 1128 . . . . . . . . . . . . . . . . . . . . . . . 24 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (š‘¢š‘‡š‘£ ā†” āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©))
6461, 63anbi12d 629 . . . . . . . . . . . . . . . . . . . . . . 23 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†” (āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©)))
65 breq12 5154 . . . . . . . . . . . . . . . . . . . . . . . 24 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (š‘”š‘‡š‘£ ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©))
66653adant2 1129 . . . . . . . . . . . . . . . . . . . . . . 23 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (š‘”š‘‡š‘£ ā†” āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©))
6764, 66imbi12d 343 . . . . . . . . . . . . . . . . . . . . . 22 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£) ā†” ((āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†’ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©)))
6859, 67anbi12d 629 . . . . . . . . . . . . . . . . . . . . 21 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ ((Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)) ā†” (Ā¬ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ© āˆ§ ((āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†’ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©))))
69 poxp.1 . . . . . . . . . . . . . . . . . . . . . . . 24 š‘‡ = {āŸØš‘„, š‘¦āŸ© āˆ£ ((š‘„ āˆˆ (š“ Ɨ šµ) āˆ§ š‘¦ āˆˆ (š“ Ɨ šµ)) āˆ§ ((1st ā€˜š‘„)š‘…(1st ā€˜š‘¦) āˆØ ((1st ā€˜š‘„) = (1st ā€˜š‘¦) āˆ§ (2nd ā€˜š‘„)š‘†(2nd ā€˜š‘¦))))}
7069xporderlem 8117 . . . . . . . . . . . . . . . . . . . . . . 23 (āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ© ā†” (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
7170notbii 319 . . . . . . . . . . . . . . . . . . . . . 22 (Ā¬ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ© ā†” Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))))
7269xporderlem 8117 . . . . . . . . . . . . . . . . . . . . . . . 24 (āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© ā†” (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))))
7369xporderlem 8117 . . . . . . . . . . . . . . . . . . . . . . . 24 (āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ© ā†” (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“))))
7472, 73anbi12i 625 . . . . . . . . . . . . . . . . . . . . . . 23 ((āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†” ((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))))
7569xporderlem 8117 . . . . . . . . . . . . . . . . . . . . . . 23 (āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ© ā†” (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))
7674, 75imbi12i 349 . . . . . . . . . . . . . . . . . . . . . 22 (((āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†’ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†” (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))
7771, 76anbi12i 625 . . . . . . . . . . . . . . . . . . . . 21 ((Ā¬ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘Ž, š‘āŸ© āˆ§ ((āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘, š‘‘āŸ© āˆ§ āŸØš‘, š‘‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©) ā†’ āŸØš‘Ž, š‘āŸ©š‘‡āŸØš‘’, š‘“āŸ©)) ā†” (Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))) āˆ§ (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“))))))
7868, 77bitrdi 286 . . . . . . . . . . . . . . . . . . . 20 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ ((Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)) ā†” (Ā¬ (((š‘Ž āˆˆ š“ āˆ§ š‘Ž āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘Ž āˆØ (š‘Ž = š‘Ž āˆ§ š‘š‘†š‘))) āˆ§ (((((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘ āˆØ (š‘Ž = š‘ āˆ§ š‘š‘†š‘‘))) āˆ§ (((š‘ āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘š‘…š‘’ āˆØ (š‘ = š‘’ āˆ§ š‘‘š‘†š‘“)))) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘’ āˆˆ š“) āˆ§ (š‘ āˆˆ šµ āˆ§ š‘“ āˆˆ šµ)) āˆ§ (š‘Žš‘…š‘’ āˆØ (š‘Ž = š‘’ āˆ§ š‘š‘†š‘“)))))))
7955, 78imbitrrid 245 . . . . . . . . . . . . . . . . . . 19 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
8079expcomd 415 . . . . . . . . . . . . . . . . . 18 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) ā†’ (((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))))
8180imp 405 . . . . . . . . . . . . . . . . 17 (((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ š‘£ = āŸØš‘’, š‘“āŸ©) āˆ§ ((š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ) āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ) āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
824, 81sylbi 216 . . . . . . . . . . . . . . . 16 (((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) āˆ§ (š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ (š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
83823exp 1117 . . . . . . . . . . . . . . 15 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ ((š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ ((š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8483com3l 89 . . . . . . . . . . . . . 14 ((š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ ((š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8584exlimivv 1933 . . . . . . . . . . . . 13 (āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ ((š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8685com3l 89 . . . . . . . . . . . 12 ((š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ (āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8786exlimivv 1933 . . . . . . . . . . 11 (āˆƒš‘’āˆƒš‘“(š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ (āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8887com3l 89 . . . . . . . . . 10 ((š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ (āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ (āˆƒš‘’āˆƒš‘“(š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
8988exlimivv 1933 . . . . . . . . 9 (āˆƒš‘Žāˆƒš‘(š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) ā†’ (āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) ā†’ (āˆƒš‘’āˆƒš‘“(š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))))
90893imp 1109 . . . . . . . 8 ((āˆƒš‘Žāˆƒš‘(š‘” = āŸØš‘Ž, š‘āŸ© āˆ§ (š‘Ž āˆˆ š“ āˆ§ š‘ āˆˆ šµ)) āˆ§ āˆƒš‘āˆƒš‘‘(š‘¢ = āŸØš‘, š‘‘āŸ© āˆ§ (š‘ āˆˆ š“ āˆ§ š‘‘ āˆˆ šµ)) āˆ§ āˆƒš‘’āˆƒš‘“(š‘£ = āŸØš‘’, š‘“āŸ© āˆ§ (š‘’ āˆˆ š“ āˆ§ š‘“ āˆˆ šµ))) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
911, 2, 3, 90syl3anb 1159 . . . . . . 7 ((š‘” āˆˆ (š“ Ɨ šµ) āˆ§ š‘¢ āˆˆ (š“ Ɨ šµ) āˆ§ š‘£ āˆˆ (š“ Ɨ šµ)) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
92913expia 1119 . . . . . 6 ((š‘” āˆˆ (š“ Ɨ šµ) āˆ§ š‘¢ āˆˆ (š“ Ɨ šµ)) ā†’ (š‘£ āˆˆ (š“ Ɨ šµ) ā†’ ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))))
9392com3r 87 . . . . 5 ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ ((š‘” āˆˆ (š“ Ɨ šµ) āˆ§ š‘¢ āˆˆ (š“ Ɨ šµ)) ā†’ (š‘£ āˆˆ (š“ Ɨ šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))))
9493imp 405 . . . 4 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ (š‘” āˆˆ (š“ Ɨ šµ) āˆ§ š‘¢ āˆˆ (š“ Ɨ šµ))) ā†’ (š‘£ āˆˆ (š“ Ɨ šµ) ā†’ (Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£))))
9594ralrimiv 3143 . . 3 (((š‘… Po š“ āˆ§ š‘† Po šµ) āˆ§ (š‘” āˆˆ (š“ Ɨ šµ) āˆ§ š‘¢ āˆˆ (š“ Ɨ šµ))) ā†’ āˆ€š‘£ āˆˆ (š“ Ɨ šµ)(Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))
9695ralrimivva 3198 . 2 ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ āˆ€š‘” āˆˆ (š“ Ɨ šµ)āˆ€š‘¢ āˆˆ (š“ Ɨ šµ)āˆ€š‘£ āˆˆ (š“ Ɨ šµ)(Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))
97 df-po 5589 . 2 (š‘‡ Po (š“ Ɨ šµ) ā†” āˆ€š‘” āˆˆ (š“ Ɨ šµ)āˆ€š‘¢ āˆˆ (š“ Ɨ šµ)āˆ€š‘£ āˆˆ (š“ Ɨ šµ)(Ā¬ š‘”š‘‡š‘” āˆ§ ((š‘”š‘‡š‘¢ āˆ§ š‘¢š‘‡š‘£) ā†’ š‘”š‘‡š‘£)))
9896, 97sylibr 233 1 ((š‘… Po š“ āˆ§ š‘† Po šµ) ā†’ š‘‡ Po (š“ Ɨ šµ))
Colors of variables: wff setvar class
Syntax hints:  Ā¬ wn 3   ā†’ wi 4   ā†” wb 205   āˆ§ wa 394   āˆØ wo 843   āˆ§ w3a 1085   = wceq 1539  āˆƒwex 1779   āˆˆ wcel 2104  āˆ€wral 3059  āŸØcop 4635   class class class wbr 5149  {copab 5211   Po wpo 5587   Ɨ cxp 5675  ā€˜cfv 6544  1st c1st 7977  2nd c2nd 7978
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-11 2152  ax-12 2169  ax-ext 2701  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7729
This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2532  df-eu 2561  df-clab 2708  df-cleq 2722  df-clel 2808  df-nfc 2883  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-uni 4910  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-po 5589  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-iota 6496  df-fun 6546  df-fv 6552  df-1st 7979  df-2nd 7980
This theorem is referenced by:  soxp  8119
  Copyright terms: Public domain W3C validator