Description: The value of _K1 is bounded by its argument. Part of Proposition 15.10(1) of TakeutiZaring p. 156. (Contributed by BTernaryTau, 12-Oct-2026)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | k1le | |- ( A e. On -> ( _K1 ` A ) C_ A ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | k1on | |- ( _K1 ` A ) e. On |
|
| 2 | k2on | |- ( _K2 ` A ) e. On |
|
| 3 | maxssj0 | |- ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) |
|
| 4 | 1 2 3 | mp2an | |- ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) |
| 5 | j0le | |- ( A e. On -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ A ) |
|
| 6 | 4 5 | sstrid | |- ( A e. On -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ A ) |
| 7 | 6 | unssad | |- ( A e. On -> ( _K1 ` A ) C_ A ) |