Step | Hyp | Ref
| Expression |
1 | | elreal2 11075 |
. . . . . . 7
β’ (π₯ β β β
((1st βπ₯)
β R β§ π₯ = β¨(1st βπ₯),
0Rβ©)) |
2 | 1 | simplbi 499 |
. . . . . 6
β’ (π₯ β β β
(1st βπ₯)
β R) |
3 | 2 | adantl 483 |
. . . . 5
β’ (((π΄ β β β§ π΄ β β
) β§ π₯ β β) β
(1st βπ₯)
β R) |
4 | | fo1st 7946 |
. . . . . . . . . . . 12
β’
1st :VβontoβV |
5 | | fof 6761 |
. . . . . . . . . . . 12
β’
(1st :VβontoβV β 1st
:VβΆV) |
6 | | ffn 6673 |
. . . . . . . . . . . 12
β’
(1st :VβΆV β 1st Fn V) |
7 | 4, 5, 6 | mp2b 10 |
. . . . . . . . . . 11
β’
1st Fn V |
8 | | ssv 3973 |
. . . . . . . . . . 11
β’ π΄ β V |
9 | | fvelimab 6919 |
. . . . . . . . . . 11
β’
((1st Fn V β§ π΄ β V) β (π€ β (1st β π΄) β βπ¦ β π΄ (1st βπ¦) = π€)) |
10 | 7, 8, 9 | mp2an 691 |
. . . . . . . . . 10
β’ (π€ β (1st β
π΄) β βπ¦ β π΄ (1st βπ¦) = π€) |
11 | | r19.29 3118 |
. . . . . . . . . . . 12
β’
((βπ¦ β
π΄ π¦ <β π₯ β§ βπ¦ β π΄ (1st βπ¦) = π€) β βπ¦ β π΄ (π¦ <β π₯ β§ (1st βπ¦) = π€)) |
12 | | ssel2 3944 |
. . . . . . . . . . . . . . . . 17
β’ ((π΄ β β β§ π¦ β π΄) β π¦ β β) |
13 | | ltresr2 11084 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((π¦ β β β§ π₯ β β) β (π¦ <β π₯ β (1st
βπ¦)
<R (1st βπ₯))) |
14 | | breq1 5113 |
. . . . . . . . . . . . . . . . . . . 20
β’
((1st βπ¦) = π€ β ((1st βπ¦) <R
(1st βπ₯)
β π€
<R (1st βπ₯))) |
15 | 13, 14 | sylan9bb 511 |
. . . . . . . . . . . . . . . . . . 19
β’ (((π¦ β β β§ π₯ β β) β§
(1st βπ¦) =
π€) β (π¦ <β π₯ β π€ <R
(1st βπ₯))) |
16 | 15 | biimpd 228 |
. . . . . . . . . . . . . . . . . 18
β’ (((π¦ β β β§ π₯ β β) β§
(1st βπ¦) =
π€) β (π¦ <β π₯ β π€ <R
(1st βπ₯))) |
17 | 16 | exp31 421 |
. . . . . . . . . . . . . . . . 17
β’ (π¦ β β β (π₯ β β β
((1st βπ¦)
= π€ β (π¦ <β π₯ β π€ <R
(1st βπ₯))))) |
18 | 12, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ ((π΄ β β β§ π¦ β π΄) β (π₯ β β β ((1st
βπ¦) = π€ β (π¦ <β π₯ β π€ <R
(1st βπ₯))))) |
19 | 18 | imp4b 423 |
. . . . . . . . . . . . . . 15
β’ (((π΄ β β β§ π¦ β π΄) β§ π₯ β β) β (((1st
βπ¦) = π€ β§ π¦ <β π₯) β π€ <R
(1st βπ₯))) |
20 | 19 | ancomsd 467 |
. . . . . . . . . . . . . 14
β’ (((π΄ β β β§ π¦ β π΄) β§ π₯ β β) β ((π¦ <β π₯ β§ (1st βπ¦) = π€) β π€ <R
(1st βπ₯))) |
21 | 20 | an32s 651 |
. . . . . . . . . . . . 13
β’ (((π΄ β β β§ π₯ β β) β§ π¦ β π΄) β ((π¦ <β π₯ β§ (1st βπ¦) = π€) β π€ <R
(1st βπ₯))) |
22 | 21 | rexlimdva 3153 |
. . . . . . . . . . . 12
β’ ((π΄ β β β§ π₯ β β) β
(βπ¦ β π΄ (π¦ <β π₯ β§ (1st βπ¦) = π€) β π€ <R
(1st βπ₯))) |
23 | 11, 22 | syl5 34 |
. . . . . . . . . . 11
β’ ((π΄ β β β§ π₯ β β) β
((βπ¦ β π΄ π¦ <β π₯ β§ βπ¦ β π΄ (1st βπ¦) = π€) β π€ <R
(1st βπ₯))) |
24 | 23 | expd 417 |
. . . . . . . . . 10
β’ ((π΄ β β β§ π₯ β β) β
(βπ¦ β π΄ π¦ <β π₯ β (βπ¦ β π΄ (1st βπ¦) = π€ β π€ <R
(1st βπ₯)))) |
25 | 10, 24 | syl7bi 255 |
. . . . . . . . 9
β’ ((π΄ β β β§ π₯ β β) β
(βπ¦ β π΄ π¦ <β π₯ β (π€ β (1st β π΄) β π€ <R
(1st βπ₯)))) |
26 | 25 | impr 456 |
. . . . . . . 8
β’ ((π΄ β β β§ (π₯ β β β§
βπ¦ β π΄ π¦ <β π₯)) β (π€ β (1st β π΄) β π€ <R
(1st βπ₯))) |
27 | 26 | adantlr 714 |
. . . . . . 7
β’ (((π΄ β β β§ π΄ β β
) β§ (π₯ β β β§
βπ¦ β π΄ π¦ <β π₯)) β (π€ β (1st β π΄) β π€ <R
(1st βπ₯))) |
28 | 27 | ralrimiv 3143 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β β
) β§ (π₯ β β β§
βπ¦ β π΄ π¦ <β π₯)) β βπ€ β (1st β π΄)π€ <R
(1st βπ₯)) |
29 | 28 | expr 458 |
. . . . 5
β’ (((π΄ β β β§ π΄ β β
) β§ π₯ β β) β
(βπ¦ β π΄ π¦ <β π₯ β βπ€ β (1st β π΄)π€ <R
(1st βπ₯))) |
30 | | brralrspcev 5170 |
. . . . 5
β’
(((1st βπ₯) β R β§ βπ€ β (1st β
π΄)π€ <R
(1st βπ₯))
β βπ£ β
R βπ€
β (1st β π΄)π€ <R π£) |
31 | 3, 29, 30 | syl6an 683 |
. . . 4
β’ (((π΄ β β β§ π΄ β β
) β§ π₯ β β) β
(βπ¦ β π΄ π¦ <β π₯ β βπ£ β R βπ€ β (1st β
π΄)π€ <R π£)) |
32 | 31 | rexlimdva 3153 |
. . 3
β’ ((π΄ β β β§ π΄ β β
) β
(βπ₯ β β
βπ¦ β π΄ π¦ <β π₯ β βπ£ β R βπ€ β (1st β
π΄)π€ <R π£)) |
33 | | n0 4311 |
. . . . . 6
β’ (π΄ β β
β
βπ¦ π¦ β π΄) |
34 | | fnfvima 7188 |
. . . . . . . . 9
β’
((1st Fn V β§ π΄ β V β§ π¦ β π΄) β (1st βπ¦) β (1st β
π΄)) |
35 | 7, 8, 34 | mp3an12 1452 |
. . . . . . . 8
β’ (π¦ β π΄ β (1st βπ¦) β (1st β
π΄)) |
36 | 35 | ne0d 4300 |
. . . . . . 7
β’ (π¦ β π΄ β (1st β π΄) β β
) |
37 | 36 | exlimiv 1934 |
. . . . . 6
β’
(βπ¦ π¦ β π΄ β (1st β π΄) β β
) |
38 | 33, 37 | sylbi 216 |
. . . . 5
β’ (π΄ β β
β
(1st β π΄)
β β
) |
39 | | supsr 11055 |
. . . . . 6
β’
(((1st β π΄) β β
β§ βπ£ β R
βπ€ β
(1st β π΄)π€ <R π£) β βπ£ β R
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β§ βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’))) |
40 | 39 | ex 414 |
. . . . 5
β’
((1st β π΄) β β
β (βπ£ β R
βπ€ β
(1st β π΄)π€ <R π£ β βπ£ β R
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β§ βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’)))) |
41 | 38, 40 | syl 17 |
. . . 4
β’ (π΄ β β
β
(βπ£ β
R βπ€
β (1st β π΄)π€ <R π£ β βπ£ β R
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β§ βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’)))) |
42 | 41 | adantl 483 |
. . 3
β’ ((π΄ β β β§ π΄ β β
) β
(βπ£ β
R βπ€
β (1st β π΄)π€ <R π£ β βπ£ β R
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β§ βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’)))) |
43 | | breq2 5114 |
. . . . . . . . . . . 12
β’ (π€ = (1st βπ¦) β (π£ <R π€ β π£ <R
(1st βπ¦))) |
44 | 43 | notbid 318 |
. . . . . . . . . . 11
β’ (π€ = (1st βπ¦) β (Β¬ π£ <R
π€ β Β¬ π£ <R
(1st βπ¦))) |
45 | 44 | rspccv 3581 |
. . . . . . . . . 10
β’
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β ((1st βπ¦) β (1st β
π΄) β Β¬ π£ <R
(1st βπ¦))) |
46 | 35, 45 | syl5com 31 |
. . . . . . . . 9
β’ (π¦ β π΄ β (βπ€ β (1st β π΄) Β¬ π£ <R π€ β Β¬ π£ <R
(1st βπ¦))) |
47 | 46 | adantl 483 |
. . . . . . . 8
β’ ((π΄ β β β§ π¦ β π΄) β (βπ€ β (1st β π΄) Β¬ π£ <R π€ β Β¬ π£ <R
(1st βπ¦))) |
48 | | elreal2 11075 |
. . . . . . . . . . . . 13
β’ (π¦ β β β
((1st βπ¦)
β R β§ π¦ = β¨(1st βπ¦),
0Rβ©)) |
49 | 48 | simprbi 498 |
. . . . . . . . . . . 12
β’ (π¦ β β β π¦ = β¨(1st
βπ¦),
0Rβ©) |
50 | 49 | breq2d 5122 |
. . . . . . . . . . 11
β’ (π¦ β β β
(β¨π£,
0Rβ© <β π¦ β β¨π£, 0Rβ©
<β β¨(1st βπ¦),
0Rβ©)) |
51 | | ltresr 11083 |
. . . . . . . . . . 11
β’
(β¨π£,
0Rβ© <β β¨(1st
βπ¦),
0Rβ© β π£ <R
(1st βπ¦)) |
52 | 50, 51 | bitrdi 287 |
. . . . . . . . . 10
β’ (π¦ β β β
(β¨π£,
0Rβ© <β π¦ β π£ <R
(1st βπ¦))) |
53 | 12, 52 | syl 17 |
. . . . . . . . 9
β’ ((π΄ β β β§ π¦ β π΄) β (β¨π£, 0Rβ©
<β π¦
β π£
<R (1st βπ¦))) |
54 | 53 | notbid 318 |
. . . . . . . 8
β’ ((π΄ β β β§ π¦ β π΄) β (Β¬ β¨π£, 0Rβ©
<β π¦
β Β¬ π£
<R (1st βπ¦))) |
55 | 47, 54 | sylibrd 259 |
. . . . . . 7
β’ ((π΄ β β β§ π¦ β π΄) β (βπ€ β (1st β π΄) Β¬ π£ <R π€ β Β¬ β¨π£,
0Rβ© <β π¦)) |
56 | 55 | ralrimdva 3152 |
. . . . . 6
β’ (π΄ β β β
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦)) |
57 | 56 | ad2antrr 725 |
. . . . 5
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
(βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦)) |
58 | 49 | breq1d 5120 |
. . . . . . . . . . . . . 14
β’ (π¦ β β β (π¦ <β
β¨π£,
0Rβ© β β¨(1st βπ¦),
0Rβ© <β β¨π£,
0Rβ©)) |
59 | | ltresr 11083 |
. . . . . . . . . . . . . 14
β’
(β¨(1st βπ¦), 0Rβ©
<β β¨π£, 0Rβ© β
(1st βπ¦)
<R π£) |
60 | 58, 59 | bitrdi 287 |
. . . . . . . . . . . . 13
β’ (π¦ β β β (π¦ <β
β¨π£,
0Rβ© β (1st βπ¦) <R
π£)) |
61 | 48 | simplbi 499 |
. . . . . . . . . . . . . . 15
β’ (π¦ β β β
(1st βπ¦)
β R) |
62 | | breq1 5113 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = (1st βπ¦) β (π€ <R π£ β (1st
βπ¦)
<R π£)) |
63 | | breq1 5113 |
. . . . . . . . . . . . . . . . . 18
β’ (π€ = (1st βπ¦) β (π€ <R π’ β (1st
βπ¦)
<R π’)) |
64 | 63 | rexbidv 3176 |
. . . . . . . . . . . . . . . . 17
β’ (π€ = (1st βπ¦) β (βπ’ β (1st β
π΄)π€ <R π’ β βπ’ β (1st β
π΄)(1st
βπ¦)
<R π’)) |
65 | 62, 64 | imbi12d 345 |
. . . . . . . . . . . . . . . 16
β’ (π€ = (1st βπ¦) β ((π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’) β ((1st
βπ¦)
<R π£ β βπ’ β (1st β π΄)(1st βπ¦) <R
π’))) |
66 | 65 | rspccv 3581 |
. . . . . . . . . . . . . . 15
β’
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β ((1st
βπ¦) β
R β ((1st βπ¦) <R π£ β βπ’ β (1st β
π΄)(1st
βπ¦)
<R π’))) |
67 | 61, 66 | syl5 34 |
. . . . . . . . . . . . . 14
β’
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β (π¦ β β β ((1st
βπ¦)
<R π£ β βπ’ β (1st β π΄)(1st βπ¦) <R
π’))) |
68 | 67 | com3l 89 |
. . . . . . . . . . . . 13
β’ (π¦ β β β
((1st βπ¦)
<R π£ β (βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’) β βπ’ β (1st β
π΄)(1st
βπ¦)
<R π’))) |
69 | 60, 68 | sylbid 239 |
. . . . . . . . . . . 12
β’ (π¦ β β β (π¦ <β
β¨π£,
0Rβ© β (βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’) β βπ’ β (1st β
π΄)(1st
βπ¦)
<R π’))) |
70 | 69 | adantr 482 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π΄ β β) β (π¦ <β
β¨π£,
0Rβ© β (βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’) β βπ’ β (1st β
π΄)(1st
βπ¦)
<R π’))) |
71 | | fvelimab 6919 |
. . . . . . . . . . . . . . . 16
β’
((1st Fn V β§ π΄ β V) β (π’ β (1st β π΄) β βπ§ β π΄ (1st βπ§) = π’)) |
72 | 7, 8, 71 | mp2an 691 |
. . . . . . . . . . . . . . 15
β’ (π’ β (1st β
π΄) β βπ§ β π΄ (1st βπ§) = π’) |
73 | | ssel2 3944 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π΄ β β β§ π§ β π΄) β π§ β β) |
74 | | ltresr2 11084 |
. . . . . . . . . . . . . . . . . . . . . 22
β’ ((π¦ β β β§ π§ β β) β (π¦ <β π§ β (1st
βπ¦)
<R (1st βπ§))) |
75 | 73, 74 | sylan2 594 |
. . . . . . . . . . . . . . . . . . . . 21
β’ ((π¦ β β β§ (π΄ β β β§ π§ β π΄)) β (π¦ <β π§ β (1st βπ¦) <R
(1st βπ§))) |
76 | | breq2 5114 |
. . . . . . . . . . . . . . . . . . . . 21
β’
((1st βπ§) = π’ β ((1st βπ¦) <R
(1st βπ§)
β (1st βπ¦) <R π’)) |
77 | 75, 76 | sylan9bb 511 |
. . . . . . . . . . . . . . . . . . . 20
β’ (((π¦ β β β§ (π΄ β β β§ π§ β π΄)) β§ (1st βπ§) = π’) β (π¦ <β π§ β (1st βπ¦) <R
π’)) |
78 | 77 | exbiri 810 |
. . . . . . . . . . . . . . . . . . 19
β’ ((π¦ β β β§ (π΄ β β β§ π§ β π΄)) β ((1st βπ§) = π’ β ((1st βπ¦) <R
π’ β π¦ <β π§))) |
79 | 78 | expr 458 |
. . . . . . . . . . . . . . . . . 18
β’ ((π¦ β β β§ π΄ β β) β (π§ β π΄ β ((1st βπ§) = π’ β ((1st βπ¦) <R
π’ β π¦ <β π§)))) |
80 | 79 | com4r 94 |
. . . . . . . . . . . . . . . . 17
β’
((1st βπ¦) <R π’ β ((π¦ β β β§ π΄ β β) β (π§ β π΄ β ((1st βπ§) = π’ β π¦ <β π§)))) |
81 | 80 | imp 408 |
. . . . . . . . . . . . . . . 16
β’
(((1st βπ¦) <R π’ β§ (π¦ β β β§ π΄ β β)) β (π§ β π΄ β ((1st βπ§) = π’ β π¦ <β π§))) |
82 | 81 | reximdvai 3163 |
. . . . . . . . . . . . . . 15
β’
(((1st βπ¦) <R π’ β§ (π¦ β β β§ π΄ β β)) β (βπ§ β π΄ (1st βπ§) = π’ β βπ§ β π΄ π¦ <β π§)) |
83 | 72, 82 | biimtrid 241 |
. . . . . . . . . . . . . 14
β’
(((1st βπ¦) <R π’ β§ (π¦ β β β§ π΄ β β)) β (π’ β (1st β
π΄) β βπ§ β π΄ π¦ <β π§)) |
84 | 83 | expcom 415 |
. . . . . . . . . . . . 13
β’ ((π¦ β β β§ π΄ β β) β
((1st βπ¦)
<R π’ β (π’ β (1st β π΄) β βπ§ β π΄ π¦ <β π§))) |
85 | 84 | com23 86 |
. . . . . . . . . . . 12
β’ ((π¦ β β β§ π΄ β β) β (π’ β (1st β
π΄) β ((1st
βπ¦)
<R π’ β βπ§ β π΄ π¦ <β π§))) |
86 | 85 | rexlimdv 3151 |
. . . . . . . . . . 11
β’ ((π¦ β β β§ π΄ β β) β
(βπ’ β
(1st β π΄)(1st βπ¦) <R π’ β βπ§ β π΄ π¦ <β π§)) |
87 | 70, 86 | syl6d 75 |
. . . . . . . . . 10
β’ ((π¦ β β β§ π΄ β β) β (π¦ <β
β¨π£,
0Rβ© β (βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’) β βπ§ β π΄ π¦ <β π§))) |
88 | 87 | com23 86 |
. . . . . . . . 9
β’ ((π¦ β β β§ π΄ β β) β
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§))) |
89 | 88 | ex 414 |
. . . . . . . 8
β’ (π¦ β β β (π΄ β β β
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§)))) |
90 | 89 | com3l 89 |
. . . . . . 7
β’ (π΄ β β β
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β (π¦ β β β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§)))) |
91 | 90 | ad2antrr 725 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β (π¦ β β β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§)))) |
92 | 91 | ralrimdv 3150 |
. . . . 5
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
(βπ€ β
R (π€
<R π£ β βπ’ β (1st β π΄)π€ <R π’) β βπ¦ β β (π¦ <β
β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§))) |
93 | | opelreal 11073 |
. . . . . . . 8
β’
(β¨π£,
0Rβ© β β β π£ β R) |
94 | 93 | biimpri 227 |
. . . . . . 7
β’ (π£ β R β
β¨π£,
0Rβ© β β) |
95 | 94 | adantl 483 |
. . . . . 6
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
β¨π£,
0Rβ© β β) |
96 | | breq1 5113 |
. . . . . . . . . . 11
β’ (π₯ = β¨π£, 0Rβ© β
(π₯ <β
π¦ β β¨π£,
0Rβ© <β π¦)) |
97 | 96 | notbid 318 |
. . . . . . . . . 10
β’ (π₯ = β¨π£, 0Rβ© β
(Β¬ π₯
<β π¦
β Β¬ β¨π£,
0Rβ© <β π¦)) |
98 | 97 | ralbidv 3175 |
. . . . . . . . 9
β’ (π₯ = β¨π£, 0Rβ© β
(βπ¦ β π΄ Β¬ π₯ <β π¦ β βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦)) |
99 | | breq2 5114 |
. . . . . . . . . . 11
β’ (π₯ = β¨π£, 0Rβ© β
(π¦ <β
π₯ β π¦ <β β¨π£,
0Rβ©)) |
100 | 99 | imbi1d 342 |
. . . . . . . . . 10
β’ (π₯ = β¨π£, 0Rβ© β
((π¦ <β
π₯ β βπ§ β π΄ π¦ <β π§) β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§))) |
101 | 100 | ralbidv 3175 |
. . . . . . . . 9
β’ (π₯ = β¨π£, 0Rβ© β
(βπ¦ β β
(π¦ <β
π₯ β βπ§ β π΄ π¦ <β π§) β βπ¦ β β (π¦ <β β¨π£,
0Rβ© β βπ§ β π΄ π¦ <β π§))) |
102 | 98, 101 | anbi12d 632 |
. . . . . . . 8
β’ (π₯ = β¨π£, 0Rβ© β
((βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)) β (βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦
β§ βπ¦ β
β (π¦
<β β¨π£, 0Rβ© β
βπ§ β π΄ π¦ <β π§)))) |
103 | 102 | rspcev 3584 |
. . . . . . 7
β’
((β¨π£,
0Rβ© β β β§ (βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦
β§ βπ¦ β
β (π¦
<β β¨π£, 0Rβ© β
βπ§ β π΄ π¦ <β π§))) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) |
104 | 103 | ex 414 |
. . . . . 6
β’
(β¨π£,
0Rβ© β β β ((βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦
β§ βπ¦ β
β (π¦
<β β¨π£, 0Rβ© β
βπ§ β π΄ π¦ <β π§)) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)))) |
105 | 95, 104 | syl 17 |
. . . . 5
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
((βπ¦ β π΄ Β¬ β¨π£, 0Rβ©
<β π¦
β§ βπ¦ β
β (π¦
<β β¨π£, 0Rβ© β
βπ§ β π΄ π¦ <β π§)) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)))) |
106 | 57, 92, 105 | syl2and 609 |
. . . 4
β’ (((π΄ β β β§ π΄ β β
) β§ π£ β R) β
((βπ€ β
(1st β π΄)
Β¬ π£
<R π€ β§ βπ€ β R (π€ <R π£ β βπ’ β (1st β
π΄)π€ <R π’)) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)))) |
107 | 106 | rexlimdva 3153 |
. . 3
β’ ((π΄ β β β§ π΄ β β
) β
(βπ£ β
R (βπ€
β (1st β π΄) Β¬ π£ <R π€ β§ βπ€ β R (π€ <R
π£ β βπ’ β (1st β
π΄)π€ <R π’)) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)))) |
108 | 32, 42, 107 | 3syld 60 |
. 2
β’ ((π΄ β β β§ π΄ β β
) β
(βπ₯ β β
βπ¦ β π΄ π¦ <β π₯ β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§)))) |
109 | 108 | 3impia 1118 |
1
β’ ((π΄ β β β§ π΄ β β
β§ βπ₯ β β βπ¦ β π΄ π¦ <β π₯) β βπ₯ β β (βπ¦ β π΄ Β¬ π₯ <β π¦ β§ βπ¦ β β (π¦ <β π₯ β βπ§ β π΄ π¦ <β π§))) |