Theorem k3n0k1lt

Description: The value of _K1 is strictly bounded by its argument when the value of _K3 is nonzero. Part of Proposition 15.10(2) of TakeutiZaring p. 156. (Contributed by BTernaryTau, 12-Oct-2026)

	Ref	Expression
Assertion	k3n0k1lt	Could not format assertion : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A ) with typecode |-

Proof

Step	Hyp	Ref	Expression
1		k3n0j0lt	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) with typecode |-
2		k1on	Could not format ( _K1 ` A ) e. On : No typesetting found for |- ( _K1 ` A ) e. On with typecode |-
3		k2on	Could not format ( _K2 ` A ) e. On : No typesetting found for |- ( _K2 ` A ) e. On with typecode |-
4		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 |-
5	2 3 4	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 |-
6	2 3	onun2i	Could not format ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. On : No typesetting found for |- ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. On with typecode |-
7		ontr2	Could not format ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. On /\ A e. On ) -> ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) /\ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) : No typesetting found for |- ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. On /\ A e. On ) -> ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) /\ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) with typecode |-
8	6 7	mpan	Could not format ( A e. On -> ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) /\ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) : No typesetting found for |- ( A e. On -> ( ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) C_ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) /\ ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) with typecode |-
9	5 8	mpani	Could not format ( A e. On -> ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) : No typesetting found for |- ( A e. On -> ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) with typecode |-
10	9	adantr	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( _J0 ` <. ( _K1 ` A ) , ( _K2 ` A ) >. ) e. A -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) ) with typecode |-
11	1 10	mpd	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) with typecode |-
12		onunel	Could not format ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On /\ A e. On ) -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) : No typesetting found for |- ( ( ( _K1 ` A ) e. On /\ ( _K2 ` A ) e. On /\ A e. On ) -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) with typecode |-
13	2 3 12	mp3an12	Could not format ( A e. On -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) : No typesetting found for |- ( A e. On -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) with typecode |-
14	13	adantr	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A <-> ( ( _K1 ` A ) e. A /\ ( _K2 ` A ) e. A ) ) ) with typecode |-
15	14	simprbda	Could not format ( ( ( A e. On /\ (/) e. ( _K3 ` A ) ) /\ ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) -> ( _K1 ` A ) e. A ) : No typesetting found for |- ( ( ( A e. On /\ (/) e. ( _K3 ` A ) ) /\ ( ( _K1 ` A ) u. ( _K2 ` A ) ) e. A ) -> ( _K1 ` A ) e. A ) with typecode |-
16	11 15	mpdan	Could not format ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A ) : No typesetting found for |- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A ) with typecode |-