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 ) ) )