Theorem chnrun

Description: Satisfying either of two chain relations is sufficient to make a chain under their union. (Contributed by Ender Ting, 24-Jul-2026)

	Ref	Expression
Assertion	chnrun	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∨ 𝐴 ∈ ( < Chain 𝐵 ) ) → 𝐴 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		ssun1	⊢ 𝑅 ⊆ ( 𝑅 ∪ < )
2		chnrss	⊢ ( 𝑅 ⊆ ( 𝑅 ∪ < ) → ( 𝑅 Chain 𝐵 ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
3	1 2	ax-mp	⊢ ( 𝑅 Chain 𝐵 ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 )
4	3	sseli	⊢ ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) → 𝐴 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
5		ssun2	⊢ < ⊆ ( 𝑅 ∪ < )
6		chnrss	⊢ ( < ⊆ ( 𝑅 ∪ < ) → ( < Chain 𝐵 ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
7	5 6	ax-mp	⊢ ( < Chain 𝐵 ) ⊆ ( ( 𝑅 ∪ < ) Chain 𝐵 )
8	7	sseli	⊢ ( 𝐴 ∈ ( < Chain 𝐵 ) → 𝐴 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )
9	4 8	jaoi	⊢ ( ( 𝐴 ∈ ( 𝑅 Chain 𝐵 ) ∨ 𝐴 ∈ ( < Chain 𝐵 ) ) → 𝐴 ∈ ( ( 𝑅 ∪ < ) Chain 𝐵 ) )