# Metamath Proof Explorer

## Theorem ordssun

Description: Property of a subclass of the maximum (i.e. union) of two ordinals. (Contributed by NM, 28-Nov-2003)

Ref Expression
Assertion ordssun ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({A}\subseteq {B}\cup {C}↔\left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$

### Proof

Step Hyp Ref Expression
1 ordtri2or2 ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({B}\subseteq {C}\vee {C}\subseteq {B}\right)$
2 ssequn1 ${⊢}{B}\subseteq {C}↔{B}\cup {C}={C}$
3 sseq2 ${⊢}{B}\cup {C}={C}\to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {C}\right)$
4 2 3 sylbi ${⊢}{B}\subseteq {C}\to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {C}\right)$
5 olc ${⊢}{A}\subseteq {C}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)$
6 4 5 syl6bi ${⊢}{B}\subseteq {C}\to \left({A}\subseteq {B}\cup {C}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$
7 ssequn2 ${⊢}{C}\subseteq {B}↔{B}\cup {C}={B}$
8 sseq2 ${⊢}{B}\cup {C}={B}\to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {B}\right)$
9 7 8 sylbi ${⊢}{C}\subseteq {B}\to \left({A}\subseteq {B}\cup {C}↔{A}\subseteq {B}\right)$
10 orc ${⊢}{A}\subseteq {B}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)$
11 9 10 syl6bi ${⊢}{C}\subseteq {B}\to \left({A}\subseteq {B}\cup {C}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$
12 6 11 jaoi ${⊢}\left({B}\subseteq {C}\vee {C}\subseteq {B}\right)\to \left({A}\subseteq {B}\cup {C}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$
13 1 12 syl ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({A}\subseteq {B}\cup {C}\to \left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$
14 ssun ${⊢}\left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\to {A}\subseteq {B}\cup {C}$
15 13 14 impbid1 ${⊢}\left(\mathrm{Ord}{B}\wedge \mathrm{Ord}{C}\right)\to \left({A}\subseteq {B}\cup {C}↔\left({A}\subseteq {B}\vee {A}\subseteq {C}\right)\right)$