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	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		k3n0j0lt	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 )
2		k1on	⊢ ( 𝐾1 ‘ 𝐴 ) ∈ On
3		k2on	⊢ ( 𝐾2 ‘ 𝐴 ) ∈ On
4		maxssj0	⊢ ( ( ( 𝐾1 ‘ 𝐴 ) ∈ On ∧ ( 𝐾2 ‘ 𝐴 ) ∈ On ) → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) )
5	2 3 4	mp2an	⊢ ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ )
6	2 3	onun2i	⊢ ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ On
7		ontr2	⊢ ( ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∧ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ) )
8	6 7	mpan	⊢ ( 𝐴 ∈ On → ( ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∧ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 ) → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ) )
9	5 8	mpani	⊢ ( 𝐴 ∈ On → ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ) )
10	9	adantr	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ∈ 𝐴 → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ) )
11	1 10	mpd	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 )
12		onunel	⊢ ( ( ( 𝐾1 ‘ 𝐴 ) ∈ On ∧ ( 𝐾2 ‘ 𝐴 ) ∈ On ∧ 𝐴 ∈ On ) → ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ↔ ( ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 ∧ ( 𝐾2 ‘ 𝐴 ) ∈ 𝐴 ) ) )
13	2 3 12	mp3an12	⊢ ( 𝐴 ∈ On → ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ↔ ( ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 ∧ ( 𝐾2 ‘ 𝐴 ) ∈ 𝐴 ) ) )
14	13	adantr	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ↔ ( ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 ∧ ( 𝐾2 ‘ 𝐴 ) ∈ 𝐴 ) ) )
15	14	simprbda	⊢ ( ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) ∧ ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ∈ 𝐴 ) → ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 )
16	11 15	mpdan	⊢ ( ( 𝐴 ∈ On ∧ ∅ ∈ ( 𝐾3 ‘ 𝐴 ) ) → ( 𝐾1 ‘ 𝐴 ) ∈ 𝐴 )