Step | Hyp | Ref
| Expression |
1 | | suplocexpr.ub |
. . . 4
ā¢ (š ā āš„ ā P āš¦ ā š“ š¦<P š„) |
2 | | prop 7473 |
. . . . . . 7
ā¢ (š„ ā P ā
āØ(1st āš„), (2nd āš„)ā© ā
P) |
3 | | prmu 7476 |
. . . . . . 7
ā¢
(āØ(1st āš„), (2nd āš„)ā© ā P ā
āš ā
Q š ā
(2nd āš„)) |
4 | 2, 3 | syl 14 |
. . . . . 6
ā¢ (š„ ā P ā
āš ā
Q š ā
(2nd āš„)) |
5 | 4 | ad2antrl 490 |
. . . . 5
ā¢ ((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā āš ā Q š ā (2nd
āš„)) |
6 | | fo2nd 6158 |
. . . . . . . . . . . . 13
ā¢
2nd :VāontoāV |
7 | | fofun 5439 |
. . . . . . . . . . . . 13
ā¢
(2nd :VāontoāV ā Fun 2nd ) |
8 | 6, 7 | ax-mp 5 |
. . . . . . . . . . . 12
ā¢ Fun
2nd |
9 | | fvelima 5567 |
. . . . . . . . . . . 12
ā¢ ((Fun
2nd ā§ š”
ā (2nd ā š“)) ā āš¢ ā š“ (2nd āš¢) = š”) |
10 | 8, 9 | mpan 424 |
. . . . . . . . . . 11
ā¢ (š” ā (2nd ā
š“) ā āš¢ ā š“ (2nd āš¢) = š”) |
11 | 10 | adantl 277 |
. . . . . . . . . 10
ā¢
(((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā āš¢ ā š“ (2nd āš¢) = š”) |
12 | | suplocexpr.m |
. . . . . . . . . . . . . . . 16
ā¢ (š ā āš„ š„ ā š“) |
13 | | suplocexpr.loc |
. . . . . . . . . . . . . . . 16
ā¢ (š ā āš„ ā P āš¦ ā P (š„<P
š¦ ā (āš§ ā š“ š„<P š§ āØ āš§ ā š“ š§<P š¦))) |
14 | 12, 1, 13 | suplocexprlemss 7713 |
. . . . . . . . . . . . . . 15
ā¢ (š ā š“ ā P) |
15 | 14 | ad5antr 496 |
. . . . . . . . . . . . . 14
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š“ ā P) |
16 | | simprl 529 |
. . . . . . . . . . . . . 14
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š¢ ā š“) |
17 | 15, 16 | sseldd 3156 |
. . . . . . . . . . . . 13
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š¢ ā P) |
18 | | simprl 529 |
. . . . . . . . . . . . . 14
ā¢ ((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā š„ ā P) |
19 | 18 | ad4antr 494 |
. . . . . . . . . . . . 13
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š„ ā P) |
20 | | breq1 4006 |
. . . . . . . . . . . . . . 15
ā¢ (š¦ = š¢ ā (š¦<P š„ ā š¢<P š„)) |
21 | | simprr 531 |
. . . . . . . . . . . . . . . 16
ā¢ ((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā āš¦ ā š“ š¦<P š„) |
22 | 21 | ad4antr 494 |
. . . . . . . . . . . . . . 15
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā āš¦ ā š“ š¦<P š„) |
23 | 20, 22, 16 | rspcdva 2846 |
. . . . . . . . . . . . . 14
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š¢<P š„) |
24 | | ltsopr 7594 |
. . . . . . . . . . . . . . . . 17
ā¢
<P Or P |
25 | | so2nr 4321 |
. . . . . . . . . . . . . . . . 17
ā¢
((<P Or P ā§ (š¢ ā P ā§
š„ ā P))
ā Ā¬ (š¢<P š„ ā§ š„<P š¢)) |
26 | 24, 25 | mpan 424 |
. . . . . . . . . . . . . . . 16
ā¢ ((š¢ ā P ā§
š„ ā P)
ā Ā¬ (š¢<P š„ ā§ š„<P š¢)) |
27 | 17, 19, 26 | syl2anc 411 |
. . . . . . . . . . . . . . 15
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā Ā¬ (š¢<P š„ ā§ š„<P š¢)) |
28 | | imnan 690 |
. . . . . . . . . . . . . . 15
ā¢ ((š¢<P
š„ ā Ā¬ š„<P
š¢) ā Ā¬ (š¢<P
š„ ā§ š„<P š¢)) |
29 | 27, 28 | sylibr 134 |
. . . . . . . . . . . . . 14
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā (š¢<P š„ ā Ā¬ š„<P š¢)) |
30 | 23, 29 | mpd 13 |
. . . . . . . . . . . . 13
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā Ā¬ š„<P š¢) |
31 | | aptiprlemu 7638 |
. . . . . . . . . . . . 13
ā¢ ((š¢ ā P ā§
š„ ā P
ā§ Ā¬ š„<P š¢) ā (2nd
āš„) ā
(2nd āš¢)) |
32 | 17, 19, 30, 31 | syl3anc 1238 |
. . . . . . . . . . . 12
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā (2nd āš„) ā (2nd
āš¢)) |
33 | | simpllr 534 |
. . . . . . . . . . . 12
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š ā (2nd āš„)) |
34 | 32, 33 | sseldd 3156 |
. . . . . . . . . . 11
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š ā (2nd āš¢)) |
35 | | simprr 531 |
. . . . . . . . . . 11
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā (2nd āš¢) = š”) |
36 | 34, 35 | eleqtrd 2256 |
. . . . . . . . . 10
ā¢
((((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā§ (š¢ ā š“ ā§ (2nd āš¢) = š”)) ā š ā š”) |
37 | 11, 36 | rexlimddv 2599 |
. . . . . . . . 9
ā¢
(((((š ā§ (š„ ā P ā§
āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā§ š” ā (2nd ā
š“)) ā š ā š”) |
38 | 37 | ralrimiva 2550 |
. . . . . . . 8
ā¢ ((((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā
āš” ā
(2nd ā š“)š ā š”) |
39 | | vex 2740 |
. . . . . . . . 9
ā¢ š ā V |
40 | 39 | elint2 3851 |
. . . . . . . 8
ā¢ (š ā ā© (2nd ā š“) ā āš” ā (2nd ā š“)š ā š”) |
41 | 38, 40 | sylibr 134 |
. . . . . . 7
ā¢ ((((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā§ š ā (2nd
āš„)) ā š ā ā© (2nd ā š“)) |
42 | 41 | ex 115 |
. . . . . 6
ā¢ (((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā§ š ā Q) ā (š ā (2nd
āš„) ā š ā ā© (2nd ā š“))) |
43 | 42 | reximdva 2579 |
. . . . 5
ā¢ ((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā (āš ā Q š ā (2nd
āš„) ā
āš ā
Q š ā
ā© (2nd ā š“))) |
44 | 5, 43 | mpd 13 |
. . . 4
ā¢ ((š ā§ (š„ ā P ā§ āš¦ ā š“ š¦<P š„)) ā āš ā Q š ā ā© (2nd ā š“)) |
45 | 1, 44 | rexlimddv 2599 |
. . 3
ā¢ (š ā āš ā Q š ā ā©
(2nd ā š“)) |
46 | | simprr 531 |
. . . . . . 7
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā š ā ā©
(2nd ā š“)) |
47 | | simprl 529 |
. . . . . . . . 9
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā š ā Q) |
48 | | 1nq 7364 |
. . . . . . . . 9
ā¢
1Q ā Q |
49 | | addclnq 7373 |
. . . . . . . . 9
ā¢ ((š ā Q ā§
1Q ā Q) ā (š +Q
1Q) ā Q) |
50 | 47, 48, 49 | sylancl 413 |
. . . . . . . 8
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā (š +Q
1Q) ā Q) |
51 | | ltaddnq 7405 |
. . . . . . . . 9
ā¢ ((š ā Q ā§
1Q ā Q) ā š <Q (š +Q
1Q)) |
52 | 47, 48, 51 | sylancl 413 |
. . . . . . . 8
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā š <Q (š +Q
1Q)) |
53 | | breq2 4007 |
. . . . . . . . 9
ā¢ (š = (š +Q
1Q) ā (š <Q š ā š <Q (š +Q
1Q))) |
54 | 53 | rspcev 2841 |
. . . . . . . 8
ā¢ (((š +Q
1Q) ā Q ā§ š <Q (š +Q
1Q)) ā āš ā Q š <Q š) |
55 | 50, 52, 54 | syl2anc 411 |
. . . . . . 7
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā āš ā Q š <Q š) |
56 | | breq1 4006 |
. . . . . . . . 9
ā¢ (š¤ = š ā (š¤ <Q š ā š <Q š)) |
57 | 56 | rexbidv 2478 |
. . . . . . . 8
ā¢ (š¤ = š ā (āš ā Q š¤ <Q š ā āš ā Q š <Q
š)) |
58 | 57 | rspcev 2841 |
. . . . . . 7
ā¢ ((š ā ā© (2nd ā š“) ā§ āš ā Q š <Q š) ā āš¤ ā ā© (2nd ā š“)āš ā Q š¤ <Q š) |
59 | 46, 55, 58 | syl2anc 411 |
. . . . . 6
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā āš¤ ā ā©
(2nd ā š“)āš ā Q š¤ <Q š) |
60 | | rexcom 2641 |
. . . . . 6
ā¢
(āš¤ ā
ā© (2nd ā š“)āš ā Q š¤ <Q š ā āš ā Q
āš¤ ā ā© (2nd ā š“)š¤ <Q š) |
61 | 59, 60 | sylib 122 |
. . . . 5
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā āš ā Q āš¤ ā ā© (2nd ā š“)š¤ <Q š) |
62 | | ssid 3175 |
. . . . . 6
ā¢
Q ā Q |
63 | | rexss 3222 |
. . . . . 6
ā¢
(Q ā Q ā (āš ā Q
āš¤ ā ā© (2nd ā š“)š¤ <Q š ā āš ā Q (š ā Q ā§
āš¤ ā ā© (2nd ā š“)š¤ <Q š))) |
64 | 62, 63 | ax-mp 5 |
. . . . 5
ā¢
(āš ā
Q āš¤
ā ā© (2nd ā š“)š¤ <Q š ā āš ā Q (š ā Q ā§
āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
65 | 61, 64 | sylib 122 |
. . . 4
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā āš ā Q (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
66 | | suplocexpr.b |
. . . . . . . . . 10
ā¢ šµ = āØāŖ (1st ā š“), {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā© |
67 | 66 | suplocexprlem2b 7712 |
. . . . . . . . 9
ā¢ (š“ ā P ā
(2nd āšµ) =
{š¢ ā Q
ā£ āš¤ ā
ā© (2nd ā š“)š¤ <Q š¢}) |
68 | 14, 67 | syl 14 |
. . . . . . . 8
ā¢ (š ā (2nd
āšµ) = {š¢ ā Q ā£
āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}) |
69 | 68 | eleq2d 2247 |
. . . . . . 7
ā¢ (š ā (š ā (2nd āšµ) ā š ā {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢})) |
70 | | breq2 4007 |
. . . . . . . . 9
ā¢ (š¢ = š ā (š¤ <Q š¢ ā š¤ <Q š)) |
71 | 70 | rexbidv 2478 |
. . . . . . . 8
ā¢ (š¢ = š ā (āš¤ ā ā©
(2nd ā š“)š¤ <Q š¢ ā āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
72 | 71 | elrab 2893 |
. . . . . . 7
ā¢ (š ā {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢} ā (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š)) |
73 | 69, 72 | bitrdi 196 |
. . . . . 6
ā¢ (š ā (š ā (2nd āšµ) ā (š ā Q ā§ āš¤ ā ā© (2nd ā š“)š¤ <Q š))) |
74 | 73 | rexbidv 2478 |
. . . . 5
ā¢ (š ā (āš ā Q š ā (2nd āšµ) ā āš ā Q (š ā Q ā§
āš¤ ā ā© (2nd ā š“)š¤ <Q š))) |
75 | 74 | adantr 276 |
. . . 4
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā (āš ā Q š ā (2nd āšµ) ā āš ā Q (š ā Q ā§
āš¤ ā ā© (2nd ā š“)š¤ <Q š))) |
76 | 65, 75 | mpbird 167 |
. . 3
ā¢ ((š ā§ (š ā Q ā§ š ā ā© (2nd ā š“))) ā āš ā Q š ā (2nd āšµ)) |
77 | 45, 76 | rexlimddv 2599 |
. 2
ā¢ (š ā āš ā Q š ā (2nd āšµ)) |
78 | | eleq1w 2238 |
. . 3
ā¢ (š = š ā (š ā (2nd āšµ) ā š ā (2nd āšµ))) |
79 | 78 | cbvrexv 2704 |
. 2
ā¢
(āš ā
Q š ā
(2nd āšµ)
ā āš ā
Q š ā
(2nd āšµ)) |
80 | 77, 79 | sylib 122 |
1
ā¢ (š ā āš ā Q š ā (2nd āšµ)) |