r0maxss

Description: If two ordered pairs are related by _R0 , then the maximum of the first pair is less than or equal to the maximum of the second pair. (The union of two ordinals is proven to be their maximum in ordunmax .) (Contributed by BTernaryTau, 22-Sep-2026)

	Ref	Expression
Hypotheses	r0maxss.1	⊢ ( 𝜑 → 𝐴 ∈ On )
	r0maxss.2	⊢ ( 𝜑 → 𝐵 ∈ On )
	r0maxss.3	⊢ ( 𝜑 → 𝐶 ∈ On )
	r0maxss.4	⊢ ( 𝜑 → 𝐷 ∈ On )
	r0maxss.5	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ 𝑅₀ ⟨ 𝐶 , 𝐷 ⟩ )
Assertion	r0maxss	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐶 ∪ 𝐷 ) )

Proof

Step	Hyp	Ref	Expression
1		r0maxss.1	⊢ ( 𝜑 → 𝐴 ∈ On )
2		r0maxss.2	⊢ ( 𝜑 → 𝐵 ∈ On )
3		r0maxss.3	⊢ ( 𝜑 → 𝐶 ∈ On )
4		r0maxss.4	⊢ ( 𝜑 → 𝐷 ∈ On )
5		r0maxss.5	⊢ ( 𝜑 → ⟨ 𝐴 , 𝐵 ⟩ 𝑅₀ ⟨ 𝐶 , 𝐷 ⟩ )
6	1 2 3 4	brr0d	⊢ ( 𝜑 → ( ⟨ 𝐴 , 𝐵 ⟩ 𝑅₀ ⟨ 𝐶 , 𝐷 ⟩ ↔ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ) ) ) )
7	5 6	mpbid	⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ) ) )
8		simpl	⊢ ( ( ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ) → ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) )
9	8	orim2i	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ∧ ⟨ 𝐴 , 𝐵 ⟩ LexOrd ⟨ 𝐶 , 𝐷 ⟩ ) ) → ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ) )
10	7 9	syl	⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ) )
11		onun2	⊢ ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴 ∪ 𝐵 ) ∈ On )
12	1 2 11	syl2anc	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ∈ On )
13		onun2	⊢ ( ( 𝐶 ∈ On ∧ 𝐷 ∈ On ) → ( 𝐶 ∪ 𝐷 ) ∈ On )
14	3 4 13	syl2anc	⊢ ( 𝜑 → ( 𝐶 ∪ 𝐷 ) ∈ On )
15		onsseleq	⊢ ( ( ( 𝐴 ∪ 𝐵 ) ∈ On ∧ ( 𝐶 ∪ 𝐷 ) ∈ On ) → ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐶 ∪ 𝐷 ) ↔ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ) ) )
16	12 14 15	syl2anc	⊢ ( 𝜑 → ( ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐶 ∪ 𝐷 ) ↔ ( ( 𝐴 ∪ 𝐵 ) ∈ ( 𝐶 ∪ 𝐷 ) ∨ ( 𝐴 ∪ 𝐵 ) = ( 𝐶 ∪ 𝐷 ) ) ) )
17	10 16	mpbird	⊢ ( 𝜑 → ( 𝐴 ∪ 𝐵 ) ⊆ ( 𝐶 ∪ 𝐷 ) )

Metamath Proof Explorer

Theorem r0maxss

Proof