Step | Hyp | Ref
| Expression |
1 | | simpr 110 |
. . . 4
ā¢ ((š ā§ š¦<P šµ) ā š¦<P šµ) |
2 | | ltrelpr 7503 |
. . . . . . . 8
ā¢
<P ā (P Ć
P) |
3 | 2 | brel 4678 |
. . . . . . 7
ā¢ (š¦<P
šµ ā (š¦ ā P ā§
šµ ā
P)) |
4 | 3 | simpld 112 |
. . . . . 6
ā¢ (š¦<P
šµ ā š¦ ā P) |
5 | 4 | adantl 277 |
. . . . 5
ā¢ ((š ā§ š¦<P šµ) ā š¦ ā P) |
6 | 3 | simprd 114 |
. . . . . 6
ā¢ (š¦<P
šµ ā šµ ā P) |
7 | 6 | adantl 277 |
. . . . 5
ā¢ ((š ā§ š¦<P šµ) ā šµ ā P) |
8 | | ltdfpr 7504 |
. . . . 5
ā¢ ((š¦ ā P ā§
šµ ā P)
ā (š¦<P šµ ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) |
9 | 5, 7, 8 | syl2anc 411 |
. . . 4
ā¢ ((š ā§ š¦<P šµ) ā (š¦<P šµ ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) |
10 | 1, 9 | mpbid 147 |
. . 3
ā¢ ((š ā§ š¦<P šµ) ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āšµ))) |
11 | | simprrr 540 |
. . . . . 6
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā š ā (1st
āšµ)) |
12 | | suplocexpr.b |
. . . . . . . . . 10
ā¢ šµ = āØāŖ (1st ā š“), {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā© |
13 | 12 | fveq2i 5518 |
. . . . . . . . 9
ā¢
(1st āšµ) = (1st āāØāŖ (1st ā š“), {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā©) |
14 | | npex 7471 |
. . . . . . . . . . . . 13
ā¢
P ā V |
15 | 14 | a1i 9 |
. . . . . . . . . . . 12
ā¢ (š ā P ā
V) |
16 | | suplocexpr.m |
. . . . . . . . . . . . 13
ā¢ (š ā āš„ š„ ā š“) |
17 | | suplocexpr.ub |
. . . . . . . . . . . . 13
ā¢ (š ā āš„ ā P āš¦ ā š“ š¦<P š„) |
18 | | suplocexpr.loc |
. . . . . . . . . . . . 13
ā¢ (š ā āš„ ā P āš¦ ā P (š„<P
š¦ ā (āš§ ā š“ š„<P š§ āØ āš§ ā š“ š§<P š¦))) |
19 | 16, 17, 18 | suplocexprlemss 7713 |
. . . . . . . . . . . 12
ā¢ (š ā š“ ā P) |
20 | 15, 19 | ssexd 4143 |
. . . . . . . . . . 11
ā¢ (š ā š“ ā V) |
21 | | fo1st 6157 |
. . . . . . . . . . . . 13
ā¢
1st :VāontoāV |
22 | | fofun 5439 |
. . . . . . . . . . . . 13
ā¢
(1st :VāontoāV ā Fun 1st ) |
23 | 21, 22 | ax-mp 5 |
. . . . . . . . . . . 12
ā¢ Fun
1st |
24 | | funimaexg 5300 |
. . . . . . . . . . . 12
ā¢ ((Fun
1st ā§ š“
ā V) ā (1st ā š“) ā V) |
25 | 23, 24 | mpan 424 |
. . . . . . . . . . 11
ā¢ (š“ ā V ā (1st
ā š“) ā
V) |
26 | | uniexg 4439 |
. . . . . . . . . . 11
ā¢
((1st ā š“) ā V ā āŖ (1st ā š“) ā V) |
27 | 20, 25, 26 | 3syl 17 |
. . . . . . . . . 10
ā¢ (š ā āŖ (1st ā š“) ā V) |
28 | | nqex 7361 |
. . . . . . . . . . 11
ā¢
Q ā V |
29 | 28 | rabex 4147 |
. . . . . . . . . 10
ā¢ {š¢ ā Q ā£
āš¤ ā ā© (2nd ā š“)š¤ <Q š¢} ā V |
30 | | op1stg 6150 |
. . . . . . . . . 10
ā¢ ((āŖ (1st ā š“) ā V ā§ {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢} ā V) ā
(1st āāØāŖ (1st
ā š“), {š¢ ā Q ā£
āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā©) = āŖ (1st ā š“)) |
31 | 27, 29, 30 | sylancl 413 |
. . . . . . . . 9
ā¢ (š ā (1st
āāØāŖ (1st ā š“), {š¢ ā Q ā£ āš¤ ā ā© (2nd ā š“)š¤ <Q š¢}ā©) = āŖ (1st ā š“)) |
32 | 13, 31 | eqtrid 2222 |
. . . . . . . 8
ā¢ (š ā (1st
āšµ) = āŖ (1st ā š“)) |
33 | 32 | eleq2d 2247 |
. . . . . . 7
ā¢ (š ā (š ā (1st āšµ) ā š ā āŖ
(1st ā š“))) |
34 | 33 | ad2antrr 488 |
. . . . . 6
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā (š ā (1st
āšµ) ā š ā āŖ (1st ā š“))) |
35 | 11, 34 | mpbid 147 |
. . . . 5
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā š ā āŖ (1st ā š“)) |
36 | | suplocexprlemell 7711 |
. . . . 5
ā¢ (š ā āŖ (1st ā š“) ā āš§ ā š“ š ā (1st āš§)) |
37 | 35, 36 | sylib 122 |
. . . 4
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā
āš§ ā š“ š ā (1st āš§)) |
38 | | simprl 529 |
. . . . . . . . 9
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā š ā
Q) |
39 | 38 | ad2antrr 488 |
. . . . . . . 8
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š ā Q) |
40 | | simprrl 539 |
. . . . . . . . 9
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā š ā (2nd
āš¦)) |
41 | 40 | ad2antrr 488 |
. . . . . . . 8
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š ā (2nd āš¦)) |
42 | | simpr 110 |
. . . . . . . 8
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š ā (1st āš§)) |
43 | | rspe 2526 |
. . . . . . . 8
ā¢ ((š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āš§))) ā
āš ā
Q (š ā
(2nd āš¦)
ā§ š ā
(1st āš§))) |
44 | 39, 41, 42, 43 | syl12anc 1236 |
. . . . . . 7
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āš§))) |
45 | 4 | ad4antlr 495 |
. . . . . . . 8
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š¦ ā P) |
46 | 19 | ad4antr 494 |
. . . . . . . . 9
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š“ ā P) |
47 | | simplr 528 |
. . . . . . . . 9
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š§ ā š“) |
48 | 46, 47 | sseldd 3156 |
. . . . . . . 8
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š§ ā P) |
49 | | ltdfpr 7504 |
. . . . . . . 8
ā¢ ((š¦ ā P ā§
š§ ā P)
ā (š¦<P š§ ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āš§)))) |
50 | 45, 48, 49 | syl2anc 411 |
. . . . . . 7
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā (š¦<P š§ ā āš ā Q (š ā (2nd
āš¦) ā§ š ā (1st
āš§)))) |
51 | 44, 50 | mpbird 167 |
. . . . . 6
ā¢
(((((š ā§ š¦<P
šµ) ā§ (š ā Q ā§
(š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā§ š ā (1st āš§)) ā š¦<P š§) |
52 | 51 | ex 115 |
. . . . 5
ā¢ ((((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā§ š§ ā š“) ā (š ā (1st āš§) ā š¦<P š§)) |
53 | 52 | reximdva 2579 |
. . . 4
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā
(āš§ ā š“ š ā (1st āš§) ā āš§ ā š“ š¦<P š§)) |
54 | 37, 53 | mpd 13 |
. . 3
ā¢ (((š ā§ š¦<P šµ) ā§ (š ā Q ā§ (š ā (2nd
āš¦) ā§ š ā (1st
āšµ)))) ā
āš§ ā š“ š¦<P š§) |
55 | 10, 54 | rexlimddv 2599 |
. 2
ā¢ ((š ā§ š¦<P šµ) ā āš§ ā š“ š¦<P š§) |
56 | 55 | ex 115 |
1
ā¢ (š ā (š¦<P šµ ā āš§ ā š“ š¦<P š§)) |