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

Theorem suplocexprlemdisj 7719
Description: Lemma for suplocexpr 7724. The putative supremum is disjoint. (Contributed by Jim Kingdon, 9-Jan-2024.)
Hypotheses
Ref Expression
suplocexpr.m (šœ‘ ā†’ āˆƒš‘„ š‘„ āˆˆ š“)
suplocexpr.ub (šœ‘ ā†’ āˆƒš‘„ āˆˆ P āˆ€š‘¦ āˆˆ š“ š‘¦<P š‘„)
suplocexpr.loc (šœ‘ ā†’ āˆ€š‘„ āˆˆ P āˆ€š‘¦ āˆˆ P (š‘„<P š‘¦ ā†’ (āˆƒš‘§ āˆˆ š“ š‘„<P š‘§ āˆØ āˆ€š‘§ āˆˆ š“ š‘§<P š‘¦)))
suplocexpr.b šµ = āŸØāˆŖ (1st ā€œ š“), {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢}āŸ©
Assertion
Ref Expression
suplocexprlemdisj (šœ‘ ā†’ āˆ€š‘ž āˆˆ Q Ā¬ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ)))
Distinct variable groups:   š‘¤,š“,š‘¢   š‘„,š“,š‘¦   š‘¤,šµ   šœ‘,š‘ž,š‘¤   šœ‘,š‘„,š‘¦   š‘¢,š‘ž
Allowed substitution hints:   šœ‘(š‘§,š‘¢)   š“(š‘§,š‘ž)   šµ(š‘„,š‘¦,š‘§,š‘¢,š‘ž)

Proof of Theorem suplocexprlemdisj
Dummy variables š‘  š‘” are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simprl 529 . . . . 5 (((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) ā†’ š‘ž āˆˆ āˆŖ (1st ā€œ š“))
2 suplocexprlemell 7712 . . . . 5 (š‘ž āˆˆ āˆŖ (1st ā€œ š“) ā†” āˆƒš‘  āˆˆ š“ š‘ž āˆˆ (1st ā€˜š‘ ))
31, 2sylib 122 . . . 4 (((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) ā†’ āˆƒš‘  āˆˆ š“ š‘ž āˆˆ (1st ā€˜š‘ ))
4 simprr 531 . . . . . 6 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘ž āˆˆ (1st ā€˜š‘ ))
5 simplrr 536 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘ž āˆˆ (2nd ā€˜šµ))
6 suplocexpr.m . . . . . . . . . . . . 13 (šœ‘ ā†’ āˆƒš‘„ š‘„ āˆˆ š“)
7 suplocexpr.ub . . . . . . . . . . . . 13 (šœ‘ ā†’ āˆƒš‘„ āˆˆ P āˆ€š‘¦ āˆˆ š“ š‘¦<P š‘„)
8 suplocexpr.loc . . . . . . . . . . . . 13 (šœ‘ ā†’ āˆ€š‘„ āˆˆ P āˆ€š‘¦ āˆˆ P (š‘„<P š‘¦ ā†’ (āˆƒš‘§ āˆˆ š“ š‘„<P š‘§ āˆØ āˆ€š‘§ āˆˆ š“ š‘§<P š‘¦)))
96, 7, 8suplocexprlemss 7714 . . . . . . . . . . . 12 (šœ‘ ā†’ š“ āŠ† P)
109ad3antrrr 492 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š“ āŠ† P)
11 suplocexpr.b . . . . . . . . . . . . 13 šµ = āŸØāˆŖ (1st ā€œ š“), {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢}āŸ©
1211suplocexprlem2b 7713 . . . . . . . . . . . 12 (š“ āŠ† P ā†’ (2nd ā€˜šµ) = {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢})
1312eleq2d 2247 . . . . . . . . . . 11 (š“ āŠ† P ā†’ (š‘ž āˆˆ (2nd ā€˜šµ) ā†” š‘ž āˆˆ {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢}))
1410, 13syl 14 . . . . . . . . . 10 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ (š‘ž āˆˆ (2nd ā€˜šµ) ā†” š‘ž āˆˆ {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢}))
15 breq2 4008 . . . . . . . . . . . 12 (š‘¢ = š‘ž ā†’ (š‘¤ <Q š‘¢ ā†” š‘¤ <Q š‘ž))
1615rexbidv 2478 . . . . . . . . . . 11 (š‘¢ = š‘ž ā†’ (āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢ ā†” āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž))
1716elrab 2894 . . . . . . . . . 10 (š‘ž āˆˆ {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢} ā†” (š‘ž āˆˆ Q āˆ§ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž))
1814, 17bitrdi 196 . . . . . . . . 9 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ (š‘ž āˆˆ (2nd ā€˜šµ) ā†” (š‘ž āˆˆ Q āˆ§ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž)))
195, 18mpbid 147 . . . . . . . 8 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ (š‘ž āˆˆ Q āˆ§ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž))
2019simprd 114 . . . . . . 7 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž)
21 simprr 531 . . . . . . . 8 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘¤ <Q š‘ž)
2210adantr 276 . . . . . . . . . . 11 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š“ āŠ† P)
23 simplrl 535 . . . . . . . . . . 11 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘  āˆˆ š“)
2422, 23sseldd 3157 . . . . . . . . . 10 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘  āˆˆ P)
25 prop 7474 . . . . . . . . . 10 (š‘  āˆˆ P ā†’ āŸØ(1st ā€˜š‘ ), (2nd ā€˜š‘ )āŸ© āˆˆ P)
2624, 25syl 14 . . . . . . . . 9 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ āŸØ(1st ā€˜š‘ ), (2nd ā€˜š‘ )āŸ© āˆˆ P)
27 eleq2 2241 . . . . . . . . . 10 (š‘” = (2nd ā€˜š‘ ) ā†’ (š‘¤ āˆˆ š‘” ā†” š‘¤ āˆˆ (2nd ā€˜š‘ )))
28 simprl 529 . . . . . . . . . . 11 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘¤ āˆˆ āˆ© (2nd ā€œ š“))
29 vex 2741 . . . . . . . . . . . 12 š‘¤ āˆˆ V
3029elint2 3852 . . . . . . . . . . 11 (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) ā†” āˆ€š‘” āˆˆ (2nd ā€œ š“)š‘¤ āˆˆ š‘”)
3128, 30sylib 122 . . . . . . . . . 10 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ āˆ€š‘” āˆˆ (2nd ā€œ š“)š‘¤ āˆˆ š‘”)
32 fo2nd 6159 . . . . . . . . . . . . . 14 2nd :Vā€“ontoā†’V
33 fofun 5440 . . . . . . . . . . . . . 14 (2nd :Vā€“ontoā†’V ā†’ Fun 2nd )
3432, 33ax-mp 5 . . . . . . . . . . . . 13 Fun 2nd
35 vex 2741 . . . . . . . . . . . . . 14 š‘  āˆˆ V
36 fof 5439 . . . . . . . . . . . . . . . 16 (2nd :Vā€“ontoā†’V ā†’ 2nd :VāŸ¶V)
3732, 36ax-mp 5 . . . . . . . . . . . . . . 15 2nd :VāŸ¶V
3837fdmi 5374 . . . . . . . . . . . . . 14 dom 2nd = V
3935, 38eleqtrri 2253 . . . . . . . . . . . . 13 š‘  āˆˆ dom 2nd
40 funfvima 5749 . . . . . . . . . . . . 13 ((Fun 2nd āˆ§ š‘  āˆˆ dom 2nd ) ā†’ (š‘  āˆˆ š“ ā†’ (2nd ā€˜š‘ ) āˆˆ (2nd ā€œ š“)))
4134, 39, 40mp2an 426 . . . . . . . . . . . 12 (š‘  āˆˆ š“ ā†’ (2nd ā€˜š‘ ) āˆˆ (2nd ā€œ š“))
4241ad2antrl 490 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ (2nd ā€˜š‘ ) āˆˆ (2nd ā€œ š“))
4342adantr 276 . . . . . . . . . 10 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ (2nd ā€˜š‘ ) āˆˆ (2nd ā€œ š“))
4427, 31, 43rspcdva 2847 . . . . . . . . 9 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘¤ āˆˆ (2nd ā€˜š‘ ))
45 prcunqu 7484 . . . . . . . . 9 ((āŸØ(1st ā€˜š‘ ), (2nd ā€˜š‘ )āŸ© āˆˆ P āˆ§ š‘¤ āˆˆ (2nd ā€˜š‘ )) ā†’ (š‘¤ <Q š‘ž ā†’ š‘ž āˆˆ (2nd ā€˜š‘ )))
4626, 44, 45syl2anc 411 . . . . . . . 8 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ (š‘¤ <Q š‘ž ā†’ š‘ž āˆˆ (2nd ā€˜š‘ )))
4721, 46mpd 13 . . . . . . 7 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘ž āˆˆ (2nd ā€˜š‘ ))
4820, 47rexlimddv 2599 . . . . . 6 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘ž āˆˆ (2nd ā€˜š‘ ))
494, 48jca 306 . . . . 5 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ (š‘ž āˆˆ (1st ā€˜š‘ ) āˆ§ š‘ž āˆˆ (2nd ā€˜š‘ )))
50 simprl 529 . . . . . . . 8 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘  āˆˆ š“)
5110, 50sseldd 3157 . . . . . . 7 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘  āˆˆ P)
5251, 25syl 14 . . . . . 6 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ āŸØ(1st ā€˜š‘ ), (2nd ā€˜š‘ )āŸ© āˆˆ P)
53 simpllr 534 . . . . . 6 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š‘ž āˆˆ Q)
54 prdisj 7491 . . . . . 6 ((āŸØ(1st ā€˜š‘ ), (2nd ā€˜š‘ )āŸ© āˆˆ P āˆ§ š‘ž āˆˆ Q) ā†’ Ā¬ (š‘ž āˆˆ (1st ā€˜š‘ ) āˆ§ š‘ž āˆˆ (2nd ā€˜š‘ )))
5552, 53, 54syl2anc 411 . . . . 5 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ Ā¬ (š‘ž āˆˆ (1st ā€˜š‘ ) āˆ§ š‘ž āˆˆ (2nd ā€˜š‘ )))
5649, 55pm2.21fal 1373 . . . 4 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ āŠ„)
573, 56rexlimddv 2599 . . 3 (((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) ā†’ āŠ„)
5857inegd 1372 . 2 ((šœ‘ āˆ§ š‘ž āˆˆ Q) ā†’ Ā¬ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ)))
5958ralrimiva 2550 1 (šœ‘ ā†’ āˆ€š‘ž āˆˆ Q Ā¬ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ)))
Colors of variables: wff set class
Syntax hints:  Ā¬ wn 3   ā†’ wi 4   āˆ§ wa 104   ā†” wb 105   āˆØ wo 708   = wceq 1353  āŠ„wfal 1358  āˆƒwex 1492   āˆˆ wcel 2148  āˆ€wral 2455  āˆƒwrex 2456  {crab 2459  Vcvv 2738   āŠ† wss 3130  āŸØcop 3596  āˆŖ cuni 3810  āˆ© cint 3845   class class class wbr 4004  dom cdm 4627   ā€œ cima 4630  Fun wfun 5211  āŸ¶wf 5213  ā€“ontoā†’wfo 5215  ā€˜cfv 5217  1st c1st 6139  2nd c2nd 6140  Qcnq 7279   <Q cltq 7284  Pcnp 7290  <P cltp 7294
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-iinf 4588
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-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-pw 3578  df-sn 3599  df-pr 3600  df-op 3602  df-uni 3811  df-int 3846  df-iun 3889  df-br 4005  df-opab 4066  df-mpt 4067  df-id 4294  df-iom 4591  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-1st 6141  df-2nd 6142  df-qs 6541  df-ni 7303  df-nqqs 7347  df-ltnqqs 7352  df-inp 7465  df-iltp 7469
This theorem is referenced by:  suplocexprlemex  7721
  Copyright terms: Public domain W3C validator