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

Theorem suplocexprlemdisj 7721
Description: Lemma for suplocexpr 7726. 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 7714 . . . . 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 7716 . . . . . . . . . . . 12 (šœ‘ ā†’ š“ āŠ† P)
109ad3antrrr 492 . . . . . . . . . . 11 ((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) ā†’ š“ āŠ† P)
11 suplocexpr.b . . . . . . . . . . . . 13 šµ = āŸØāˆŖ (1st ā€œ š“), {š‘¢ āˆˆ Q āˆ£ āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢}āŸ©
1211suplocexprlem2b 7715 . . . . . . . . . . . 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 4009 . . . . . . . . . . . 12 (š‘¢ = š‘ž ā†’ (š‘¤ <Q š‘¢ ā†” š‘¤ <Q š‘ž))
1615rexbidv 2478 . . . . . . . . . . 11 (š‘¢ = š‘ž ā†’ (āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘¢ ā†” āˆƒš‘¤ āˆˆ āˆ© (2nd ā€œ š“)š‘¤ <Q š‘ž))
1716elrab 2895 . . . . . . . . . 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 3158 . . . . . . . . . 10 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘  āˆˆ P)
25 prop 7476 . . . . . . . . . 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 2742 . . . . . . . . . . . 12 š‘¤ āˆˆ V
3029elint2 3853 . . . . . . . . . . 11 (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) ā†” āˆ€š‘” āˆˆ (2nd ā€œ š“)š‘¤ āˆˆ š‘”)
3128, 30sylib 122 . . . . . . . . . 10 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ āˆ€š‘” āˆˆ (2nd ā€œ š“)š‘¤ āˆˆ š‘”)
32 fo2nd 6161 . . . . . . . . . . . . . 14 2nd :Vā€“ontoā†’V
33 fofun 5441 . . . . . . . . . . . . . 14 (2nd :Vā€“ontoā†’V ā†’ Fun 2nd )
3432, 33ax-mp 5 . . . . . . . . . . . . 13 Fun 2nd
35 vex 2742 . . . . . . . . . . . . . 14 š‘  āˆˆ V
36 fof 5440 . . . . . . . . . . . . . . . 16 (2nd :Vā€“ontoā†’V ā†’ 2nd :VāŸ¶V)
3732, 36ax-mp 5 . . . . . . . . . . . . . . 15 2nd :VāŸ¶V
3837fdmi 5375 . . . . . . . . . . . . . 14 dom 2nd = V
3935, 38eleqtrri 2253 . . . . . . . . . . . . 13 š‘  āˆˆ dom 2nd
40 funfvima 5750 . . . . . . . . . . . . 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 2848 . . . . . . . . 9 (((((šœ‘ āˆ§ š‘ž āˆˆ Q) āˆ§ (š‘ž āˆˆ āˆŖ (1st ā€œ š“) āˆ§ š‘ž āˆˆ (2nd ā€˜šµ))) āˆ§ (š‘  āˆˆ š“ āˆ§ š‘ž āˆˆ (1st ā€˜š‘ ))) āˆ§ (š‘¤ āˆˆ āˆ© (2nd ā€œ š“) āˆ§ š‘¤ <Q š‘ž)) ā†’ š‘¤ āˆˆ (2nd ā€˜š‘ ))
45 prcunqu 7486 . . . . . . . . 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 3158 . . . . . . 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 7493 . . . . . 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 2739   āŠ† wss 3131  āŸØcop 3597  āˆŖ cuni 3811  āˆ© cint 3846   class class class wbr 4005  dom cdm 4628   ā€œ cima 4631  Fun wfun 5212  āŸ¶wf 5214  ā€“ontoā†’wfo 5216  ā€˜cfv 5218  1st c1st 6141  2nd c2nd 6142  Qcnq 7281   <Q cltq 7286  Pcnp 7292  <P cltp 7296
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 4120  ax-sep 4123  ax-pow 4176  ax-pr 4211  ax-un 4435  ax-iinf 4589
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 2741  df-sbc 2965  df-csb 3060  df-dif 3133  df-un 3135  df-in 3137  df-ss 3144  df-pw 3579  df-sn 3600  df-pr 3601  df-op 3603  df-uni 3812  df-int 3847  df-iun 3890  df-br 4006  df-opab 4067  df-mpt 4068  df-id 4295  df-iom 4592  df-xp 4634  df-rel 4635  df-cnv 4636  df-co 4637  df-dm 4638  df-rn 4639  df-res 4640  df-ima 4641  df-iota 5180  df-fun 5220  df-fn 5221  df-f 5222  df-f1 5223  df-fo 5224  df-f1o 5225  df-fv 5226  df-1st 6143  df-2nd 6144  df-qs 6543  df-ni 7305  df-nqqs 7349  df-ltnqqs 7354  df-inp 7467  df-iltp 7471
This theorem is referenced by:  suplocexprlemex  7723
  Copyright terms: Public domain W3C validator