This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )

Proof

Step Hyp Ref Expression
1 ordtri2or2 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) )
2 ssequn1 ⊢ ( 𝐵 ⊆ 𝐶 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐶 )
3 sseq2 ⊢ ( ( 𝐵 ∪ 𝐶 ) = 𝐶 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )
4 2 3 sylbi ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐶 ) )
5 olc ⊢ ( 𝐴 ⊆ 𝐶 → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) )
6 4 5 biimtrdi ⊢ ( 𝐵 ⊆ 𝐶 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )
7 ssequn2 ⊢ ( 𝐶 ⊆ 𝐵 ↔ ( 𝐵 ∪ 𝐶 ) = 𝐵 )
8 sseq2 ⊢ ( ( 𝐵 ∪ 𝐶 ) = 𝐵 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐵 ) )
9 7 8 sylbi ⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ 𝐴 ⊆ 𝐵 ) )
10 orc ⊢ ( 𝐴 ⊆ 𝐵 → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) )
11 9 10 biimtrdi ⊢ ( 𝐶 ⊆ 𝐵 → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )
12 6 11 jaoi ⊢ ( ( 𝐵 ⊆ 𝐶 ∨ 𝐶 ⊆ 𝐵 ) → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )
13 1 12 syl ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) → ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )
14 ssun ⊢ ( ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) → 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) )
15 13 14 impbid1 ⊢ ( ( Ord 𝐵 ∧ Ord 𝐶 ) → ( 𝐴 ⊆ ( 𝐵 ∪ 𝐶 ) ↔ ( 𝐴 ⊆ 𝐵 ∨ 𝐴 ⊆ 𝐶 ) ) )