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

Metamath Proof Explorer

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