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	|- ( ( A e. On /\ (/) e. ( _K3 ` A ) ) -> ( _K1 ` A ) e. A )

Proof

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