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 ⊢Ord⁡B∧Ord⁡C→A⊆B∪C↔A⊆B∨A⊆C

Proof

Step Hyp Ref Expression
1 ordtri2or2 ⊢Ord⁡B∧Ord⁡C→B⊆C∨C⊆B
2 ssequn1 ⊢B⊆C↔B∪C=C
3 sseq2 ⊢B∪C=C→A⊆B∪C↔A⊆C
4 2 3 sylbi ⊢B⊆C→A⊆B∪C↔A⊆C
5 olc ⊢A⊆C→A⊆B∨A⊆C
6 4 5 syl6bi ⊢B⊆C→A⊆B∪C→A⊆B∨A⊆C
7 ssequn2 ⊢C⊆B↔B∪C=B
8 sseq2 ⊢B∪C=B→A⊆B∪C↔A⊆B
9 7 8 sylbi ⊢C⊆B→A⊆B∪C↔A⊆B
10 orc ⊢A⊆B→A⊆B∨A⊆C
11 9 10 syl6bi ⊢C⊆B→A⊆B∪C→A⊆B∨A⊆C
12 6 11 jaoi ⊢B⊆C∨C⊆B→A⊆B∪C→A⊆B∨A⊆C
13 1 12 syl ⊢Ord⁡B∧Ord⁡C→A⊆B∪C→A⊆B∨A⊆C
14 ssun ⊢A⊆B∨A⊆C→A⊆B∪C
15 13 14 impbid1 ⊢Ord⁡B∧Ord⁡C→A⊆B∪C↔A⊆B∨A⊆C