Theorem ordunisssuc

Description: A subclass relationship for union and successor of ordinal classes. (Contributed by NM, 28-Nov-2003)

	Ref	Expression
Assertion	ordunisssuc	|- ( ( A C_ On /\ Ord B ) -> ( U. A C_ B <-> A C_ suc B ) )

Proof

Step	Hyp	Ref	Expression
1		ssel2	|- ( ( A C_ On /\ x e. A ) -> x e. On )
2		ordsssuc	|- ( ( x e. On /\ Ord B ) -> ( x C_ B <-> x e. suc B ) )
3	1 2	sylan	|- ( ( ( A C_ On /\ x e. A ) /\ Ord B ) -> ( x C_ B <-> x e. suc B ) )
4	3	an32s	|- ( ( ( A C_ On /\ Ord B ) /\ x e. A ) -> ( x C_ B <-> x e. suc B ) )
5	4	ralbidva	|- ( ( A C_ On /\ Ord B ) -> ( A. x e. A x C_ B <-> A. x e. A x e. suc B ) )
6		unissb	|- ( U. A C_ B <-> A. x e. A x C_ B )
7		dfss3	|- ( A C_ suc B <-> A. x e. A x e. suc B )
8	5 6 7	3bitr4g	|- ( ( A C_ On /\ Ord B ) -> ( U. A C_ B <-> A C_ suc B ) )