Step | Hyp | Ref
| Expression |
1 | | simprl 529 |
. . . . 5
ā¢ (((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā š ā āŖ
(1st ā š“)) |
2 | | suplocexprlemell 7712 |
. . . . 5
ā¢ (š ā āŖ (1st ā š“) ā āš ā š“ š ā (1st āš )) |
3 | 1, 2 | sylib 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 š¦))) |
9 | 6, 7, 8 | suplocexprlemss 7714 |
. . . . . . . . . . . 12
ā¢ (š ā š“ ā P) |
10 | 9 | ad3antrrr 492 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā š“ ā P) |
11 | | suplocexpr.b |
. . . . . . . . . . . . 13
ā¢ šµ = āØāŖ (1st ā š“), {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā© |
12 | 11 | suplocexprlem2b 7713 |
. . . . . . . . . . . 12
ā¢ (š“ ā P ā
(2nd āšµ) =
{š¢ ā Q
ā£ āš¤ ā
ā© (2nd ā š“)š¤ <Q š¢}) |
13 | 12 | eleq2d 2247 |
. . . . . . . . . . 11
ā¢ (š“ ā P ā
(š ā (2nd
āšµ) ā š ā {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢})) |
14 | 10, 13 | syl 14 |
. . . . . . . . . 10
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā (š ā (2nd āšµ) ā š ā {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢})) |
15 | | breq2 4008 |
. . . . . . . . . . . 12
ā¢ (š¢ = š ā (š¤ <Q š¢ ā š¤ <Q š)) |
16 | 15 | rexbidv 2478 |
. . . . . . . . . . 11
ā¢ (š¢ = š ā (āš¤ ā ā©
(2nd ā š“)š¤ <Q š¢ ā āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
17 | 16 | elrab 2894 |
. . . . . . . . . 10
ā¢ (š ā {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢} ā (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
18 | 14, 17 | bitrdi 196 |
. . . . . . . . 9
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā (š ā (2nd āšµ) ā (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š))) |
19 | 5, 18 | mpbid 147 |
. . . . . . . 8
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
20 | 19 | simprd 114 |
. . . . . . 7
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā āš¤ ā ā© (2nd ā š“)š¤ <Q š) |
21 | | simprr 531 |
. . . . . . . 8
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š¤ <Q š) |
22 | 10 | adantr 276 |
. . . . . . . . . . 11
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š“ ā P) |
23 | | simplrl 535 |
. . . . . . . . . . 11
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š ā š“) |
24 | 22, 23 | sseldd 3157 |
. . . . . . . . . 10
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š ā P) |
25 | | prop 7474 |
. . . . . . . . . 10
ā¢ (š ā P ā
āØ(1st āš ), (2nd āš )ā© ā
P) |
26 | 24, 25 | syl 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 |
30 | 29 | elint2 3852 |
. . . . . . . . . . 11
ā¢ (š¤ ā ā© (2nd ā š“) ā āš” ā (2nd ā š“)š¤ ā š”) |
31 | 28, 30 | sylib 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 ) |
34 | 32, 33 | ax-mp 5 |
. . . . . . . . . . . . 13
ā¢ Fun
2nd |
35 | | vex 2741 |
. . . . . . . . . . . . . 14
ā¢ š ā V |
36 | | fof 5439 |
. . . . . . . . . . . . . . . 16
ā¢
(2nd :VāontoāV ā 2nd
:Vā¶V) |
37 | 32, 36 | ax-mp 5 |
. . . . . . . . . . . . . . 15
ā¢
2nd :Vā¶V |
38 | 37 | fdmi 5374 |
. . . . . . . . . . . . . 14
ā¢ dom
2nd = V |
39 | 35, 38 | eleqtrri 2253 |
. . . . . . . . . . . . 13
ā¢ š ā dom
2nd |
40 | | funfvima 5749 |
. . . . . . . . . . . . 13
ā¢ ((Fun
2nd ā§ š
ā dom 2nd ) ā (š ā š“ ā (2nd āš ) ā (2nd ā
š“))) |
41 | 34, 39, 40 | mp2an 426 |
. . . . . . . . . . . 12
ā¢ (š ā š“ ā (2nd āš ) ā (2nd ā
š“)) |
42 | 41 | ad2antrl 490 |
. . . . . . . . . . 11
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā (2nd
āš ) ā
(2nd ā š“)) |
43 | 42 | adantr 276 |
. . . . . . . . . 10
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā (2nd āš ) ā (2nd ā
š“)) |
44 | 27, 31, 43 | rspcdva 2847 |
. . . . . . . . 9
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š¤ ā (2nd āš )) |
45 | | prcunqu 7484 |
. . . . . . . . 9
ā¢
((āØ(1st āš ), (2nd āš )ā© ā P ā§ š¤ ā (2nd
āš )) ā (š¤ <Q
š ā š ā (2nd āš ))) |
46 | 26, 44, 45 | syl2anc 411 |
. . . . . . . 8
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā (š¤ <Q š ā š ā (2nd āš ))) |
47 | 21, 46 | mpd 13 |
. . . . . . 7
ā¢
(((((š ā§ š ā Q) ā§
(š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā§ (š¤ ā ā©
(2nd ā š“)
ā§ š¤
<Q š)) ā š ā (2nd āš )) |
48 | 20, 47 | rexlimddv 2599 |
. . . . . 6
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā š ā (2nd āš )) |
49 | 4, 48 | jca 306 |
. . . . 5
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā (š ā (1st āš ) ā§ š ā (2nd āš ))) |
50 | | simprl 529 |
. . . . . . . 8
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā š ā š“) |
51 | 10, 50 | sseldd 3157 |
. . . . . . 7
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā š ā P) |
52 | 51, 25 | syl 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 āš ))) |
55 | 52, 53, 54 | syl2anc 411 |
. . . . 5
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā Ā¬ (š ā (1st
āš ) ā§ š ā (2nd
āš ))) |
56 | 49, 55 | pm2.21fal 1373 |
. . . 4
ā¢ ((((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā§ (š ā š“ ā§ š ā (1st āš ))) ā
ā„) |
57 | 3, 56 | rexlimddv 2599 |
. . 3
ā¢ (((š ā§ š ā Q) ā§ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) ā
ā„) |
58 | 57 | inegd 1372 |
. 2
ā¢ ((š ā§ š ā Q) ā Ā¬ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) |
59 | 58 | ralrimiva 2550 |
1
ā¢ (š ā āš ā Q Ā¬ (š ā āŖ (1st ā š“) ā§ š ā (2nd āšµ))) |