Theorem 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	$$⊢\phi \to A\in \mathrm{On}$$
	r0maxss.2	$$⊢\phi \to B\in \mathrm{On}$$
	r0maxss.3	$$⊢\phi \to C\in \mathrm{On}$$
	r0maxss.4	$$⊢\phi \to D\in \mathrm{On}$$
	r0maxss.5	No typesetting found for |- ( ph -> <. A , B >. _R0 <. C , D >. ) with typecode |-
Assertion	r0maxss	$$⊢\phi \to A\cup B\subseteq C\cup D$$

Proof

Step	Hyp	Ref	Expression
1		r0maxss.1	$$⊢\phi \to A\in \mathrm{On}$$
2		r0maxss.2	$$⊢\phi \to B\in \mathrm{On}$$
3		r0maxss.3	$$⊢\phi \to C\in \mathrm{On}$$
4		r0maxss.4	$$⊢\phi \to D\in \mathrm{On}$$
5		r0maxss.5	Could not format ( ph -> <. A , B >. _R0 <. C , D >. ) : No typesetting found for |- ( ph -> <. A , B >. _R0 <. C , D >. ) with typecode |-
6	1 2 3 4	brr0d	Could not format ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) : No typesetting found for |- ( ph -> ( <. A , B >. _R0 <. C , D >. <-> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) ) with typecode |-
7	5 6	mpbid	Could not format ( ph -> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) : No typesetting found for |- ( ph -> ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) ) with typecode |-
8		simpl	Could not format ( ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) -> ( A u. B ) = ( C u. D ) ) : No typesetting found for |- ( ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) -> ( A u. B ) = ( C u. D ) ) with typecode |-
9	8	orim2i	Could not format ( ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) -> ( ( A u. B ) e. ( C u. D ) \/ ( A u. B ) = ( C u. D ) ) ) : No typesetting found for |- ( ( ( A u. B ) e. ( C u. D ) \/ ( ( A u. B ) = ( C u. D ) /\ <. A , B >. LexOrd <. C , D >. ) ) -> ( ( A u. B ) e. ( C u. D ) \/ ( A u. B ) = ( C u. D ) ) ) with typecode |-
10	7 9	syl	$$⊢\phi \to \left(A\cup B\in \left(C\cup D\right)\vee A\cup B=C\cup D\right)$$
11		onun2	$$⊢\left(A\in \mathrm{On}\wedge B\in \mathrm{On}\right)\to A\cup B\in \mathrm{On}$$
12	1 2 11	syl2anc	$$⊢\phi \to A\cup B\in \mathrm{On}$$
13		onun2	$$⊢\left(C\in \mathrm{On}\wedge D\in \mathrm{On}\right)\to C\cup D\in \mathrm{On}$$
14	3 4 13	syl2anc	$$⊢\phi \to C\cup D\in \mathrm{On}$$
15		onsseleq	$$⊢\left(A\cup B\in \mathrm{On}\wedge C\cup D\in \mathrm{On}\right)\to \left(A\cup B\subseteq C\cup D\leftrightarrow \left(A\cup B\in \left(C\cup D\right)\vee A\cup B=C\cup D\right)\right)$$
16	12 14 15	syl2anc	$$⊢\phi \to \left(A\cup B\subseteq C\cup D\leftrightarrow \left(A\cup B\in \left(C\cup D\right)\vee A\cup B=C\cup D\right)\right)$$
17	10 16	mpbird	$$⊢\phi \to A\cup B\subseteq C\cup D$$