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	⊢ ( 𝐴 ∈ On → ( 𝐾2 ‘ 𝐴 ) ⊆ 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		k1on	⊢ ( 𝐾1 ‘ 𝐴 ) ∈ On
2		k2on	⊢ ( 𝐾2 ‘ 𝐴 ) ∈ On
3		maxssj0	⊢ ( ( ( 𝐾1 ‘ 𝐴 ) ∈ On ∧ ( 𝐾2 ‘ 𝐴 ) ∈ On ) → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) )
4	1 2 3	mp2an	⊢ ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ )
5		j0le	⊢ ( 𝐴 ∈ On → ( 𝐽0 ‘ ⟨ ( 𝐾1 ‘ 𝐴 ) , ( 𝐾2 ‘ 𝐴 ) ⟩ ) ⊆ 𝐴 )
6	4 5	sstrid	⊢ ( 𝐴 ∈ On → ( ( 𝐾1 ‘ 𝐴 ) ∪ ( 𝐾2 ‘ 𝐴 ) ) ⊆ 𝐴 )
7	6	unssbd	⊢ ( 𝐴 ∈ On → ( 𝐾2 ‘ 𝐴 ) ⊆ 𝐴 )