Theorem k2le

Description: The value of _K2 is bounded by its argument. Part of Proposition 15.10(1) of TakeutiZaring p. 156. (Contributed by BTernaryTau, 12-Oct-2026)

	Ref	Expression
Assertion	k2le	Could not format assertion : No typesetting found for |- ( A e. On -> ( _K2 ` A ) C_ A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		k1on	Could not format ( _K1 ` A ) e. On : No typesetting found for |- ( _K1 ` A ) e. On with typecode |-
2		k2on	Could not format ( _K2 ` A ) e. On : No typesetting found for |- ( _K2 ` A ) e. On with typecode |-
3		maxssj0	Could not format ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) : No typesetting found for |- ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) ) with typecode |-
4	1 2 3	mp2an	Could not format ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) : No typesetting found for |- ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) with typecode |-
5		j0le	Could not format ( A e. On -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ A ) : No typesetting found for |- ( A e. On -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) C_ A ) with typecode |-
6	4 5	sstrid	Could not format ( A e. On -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ A ) : No typesetting found for |- ( A e. On -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ A ) with typecode |-
7	6	unssbd	Could not format ( A e. On -> ( _K2 ` A ) C_ A ) : No typesetting found for |- ( A e. On -> ( _K2 ` A ) C_ A ) with typecode |-