Step | Hyp | Ref
| Expression |
1 | | eqeq2 2748 |
. 2
β’ (+β
= if(π = β
, +β,
inf(π, β, < ))
β ((π Ramsey πΉ) = +β β (π Ramsey πΉ) = if(π = β
, +β, inf(π, β, < )))) |
2 | | eqeq2 2748 |
. 2
β’
(inf(π, β,
< ) = if(π = β
,
+β, inf(π, β,
< )) β ((π Ramsey
πΉ) = inf(π, β, < ) β (π Ramsey πΉ) = if(π = β
, +β, inf(π, β, < )))) |
3 | | ramval.c |
. . . 4
β’ πΆ = (π β V, π β β0 β¦ {π β π« π β£ (β―βπ) = π}) |
4 | | ramval.t |
. . . 4
β’ π = {π β β0 β£
βπ (π β€ (β―βπ ) β βπ β (π
βm (π πΆπ))βπ β π
βπ₯ β π« π ((πΉβπ) β€ (β―βπ₯) β§ (π₯πΆπ) β (β‘π β {π})))} |
5 | 3, 4 | ramval 16880 |
. . 3
β’ ((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β (π Ramsey πΉ) = inf(π, β*, <
)) |
6 | | infeq1 9412 |
. . . 4
β’ (π = β
β inf(π, β*, < ) =
inf(β
, β*, < )) |
7 | | xrinf0 13257 |
. . . 4
β’
inf(β
, β*, < ) = +β |
8 | 6, 7 | eqtrdi 2792 |
. . 3
β’ (π = β
β inf(π, β*, < ) =
+β) |
9 | 5, 8 | sylan9eq 2796 |
. 2
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π = β
) β (π Ramsey πΉ) = +β) |
10 | | df-ne 2944 |
. . 3
β’ (π β β
β Β¬ π = β
) |
11 | 5 | adantr 481 |
. . . 4
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β (π Ramsey πΉ) = inf(π, β*, <
)) |
12 | | xrltso 13060 |
. . . . . 6
β’ < Or
β* |
13 | 12 | a1i 11 |
. . . . 5
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β < Or
β*) |
14 | 4 | ssrab3 4040 |
. . . . . . . 8
β’ π β
β0 |
15 | | nn0ssre 12417 |
. . . . . . . 8
β’
β0 β β |
16 | 14, 15 | sstri 3953 |
. . . . . . 7
β’ π β
β |
17 | | nn0uz 12805 |
. . . . . . . . . 10
β’
β0 = (β€β₯β0) |
18 | 14, 17 | sseqtri 3980 |
. . . . . . . . 9
β’ π β
(β€β₯β0) |
19 | 18 | a1i 11 |
. . . . . . . 8
β’ ((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β π β
(β€β₯β0)) |
20 | | infssuzcl 12857 |
. . . . . . . 8
β’ ((π β
(β€β₯β0) β§ π β β
) β inf(π, β, < ) β π) |
21 | 19, 20 | sylan 580 |
. . . . . . 7
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β inf(π, β, < ) β π) |
22 | 16, 21 | sselid 3942 |
. . . . . 6
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β inf(π, β, < ) β
β) |
23 | 22 | rexrd 11205 |
. . . . 5
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β inf(π, β, < ) β
β*) |
24 | 22 | adantr 481 |
. . . . . 6
β’ ((((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β§ π§ β π) β inf(π, β, < ) β
β) |
25 | 16 | a1i 11 |
. . . . . . 7
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β π β
β) |
26 | 25 | sselda 3944 |
. . . . . 6
β’ ((((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β§ π§ β π) β π§ β β) |
27 | | simpr 485 |
. . . . . . 7
β’ ((((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β§ π§ β π) β π§ β π) |
28 | | infssuzle 12856 |
. . . . . . 7
β’ ((π β
(β€β₯β0) β§ π§ β π) β inf(π, β, < ) β€ π§) |
29 | 18, 27, 28 | sylancr 587 |
. . . . . 6
β’ ((((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β§ π§ β π) β inf(π, β, < ) β€ π§) |
30 | 24, 26, 29 | lensymd 11306 |
. . . . 5
β’ ((((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β§ π§ β π) β Β¬ π§ < inf(π, β, < )) |
31 | 13, 23, 21, 30 | infmin 9430 |
. . . 4
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β inf(π, β*, < ) =
inf(π, β, <
)) |
32 | 11, 31 | eqtrd 2776 |
. . 3
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ π β β
) β (π Ramsey πΉ) = inf(π, β, < )) |
33 | 10, 32 | sylan2br 595 |
. 2
β’ (((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β§ Β¬
π = β
) β (π Ramsey πΉ) = inf(π, β, < )) |
34 | 1, 2, 9, 33 | ifbothda 4524 |
1
β’ ((π β β0
β§ π
β π β§ πΉ:π
βΆβ0) β (π Ramsey πΉ) = if(π = β
, +β, inf(π, β, < ))) |