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 B /\ Ord C ) -> ( A C_ ( B u. C ) <-> ( A C_ B \/ A C_ C ) ) )

Proof

Step Hyp Ref Expression
1 ordtri2or2 
 |-  ( ( Ord B /\ Ord C ) -> ( B C_ C \/ C C_ B ) )
2 ssequn1 
 |-  ( B C_ C <-> ( B u. C ) = C )
3 sseq2 
 |-  ( ( B u. C ) = C -> ( A C_ ( B u. C ) <-> A C_ C ) )
4 2 3 sylbi 
 |-  ( B C_ C -> ( A C_ ( B u. C ) <-> A C_ C ) )
5 olc 
 |-  ( A C_ C -> ( A C_ B \/ A C_ C ) )
6 4 5 biimtrdi 
 |-  ( B C_ C -> ( A C_ ( B u. C ) -> ( A C_ B \/ A C_ C ) ) )
7 ssequn2 
 |-  ( C C_ B <-> ( B u. C ) = B )
8 sseq2 
 |-  ( ( B u. C ) = B -> ( A C_ ( B u. C ) <-> A C_ B ) )
9 7 8 sylbi 
 |-  ( C C_ B -> ( A C_ ( B u. C ) <-> A C_ B ) )
10 orc 
 |-  ( A C_ B -> ( A C_ B \/ A C_ C ) )
11 9 10 biimtrdi 
 |-  ( C C_ B -> ( A C_ ( B u. C ) -> ( A C_ B \/ A C_ C ) ) )
12 6 11 jaoi 
 |-  ( ( B C_ C \/ C C_ B ) -> ( A C_ ( B u. C ) -> ( A C_ B \/ A C_ C ) ) )
13 1 12 syl 
 |-  ( ( Ord B /\ Ord C ) -> ( A C_ ( B u. C ) -> ( A C_ B \/ A C_ C ) ) )
14 ssun 
 |-  ( ( A C_ B \/ A C_ C ) -> A C_ ( B u. C ) )
15 13 14 impbid1 
 |-  ( ( Ord B /\ Ord C ) -> ( A C_ ( B u. C ) <-> ( A C_ B \/ A C_ C ) ) )