Theorem ordsucuniel

Description: Given an element A of the union of an ordinal B , suc A is an element of B itself. (Contributed by Scott Fenton, 28-Mar-2012) (Proof shortened by Mario Carneiro, 29-May-2015)

	Ref	Expression
Assertion	ordsucuniel	|- ( Ord B -> ( A e. U. B <-> suc A e. B ) )

Proof

Step	Hyp	Ref	Expression
1		orduni	|- ( Ord B -> Ord U. B )
2		ordelord	|- ( ( Ord U. B /\ A e. U. B ) -> Ord A )
3	2	ex	|- ( Ord U. B -> ( A e. U. B -> Ord A ) )
4	1 3	syl	|- ( Ord B -> ( A e. U. B -> Ord A ) )
5		ordelord	|- ( ( Ord B /\ suc A e. B ) -> Ord suc A )
6		ordsuc	|- ( Ord A <-> Ord suc A )
7	5 6	sylibr	|- ( ( Ord B /\ suc A e. B ) -> Ord A )
8	7	ex	|- ( Ord B -> ( suc A e. B -> Ord A ) )
9		ordsson	|- ( Ord B -> B C_ On )
10		ordunisssuc	|- ( ( B C_ On /\ Ord A ) -> ( U. B C_ A <-> B C_ suc A ) )
11	9 10	sylan	|- ( ( Ord B /\ Ord A ) -> ( U. B C_ A <-> B C_ suc A ) )
12		ordtri1	|- ( ( Ord U. B /\ Ord A ) -> ( U. B C_ A <-> -. A e. U. B ) )
13	1 12	sylan	|- ( ( Ord B /\ Ord A ) -> ( U. B C_ A <-> -. A e. U. B ) )
14		ordtri1	|- ( ( Ord B /\ Ord suc A ) -> ( B C_ suc A <-> -. suc A e. B ) )
15	6 14	sylan2b	|- ( ( Ord B /\ Ord A ) -> ( B C_ suc A <-> -. suc A e. B ) )
16	11 13 15	3bitr3d	|- ( ( Ord B /\ Ord A ) -> ( -. A e. U. B <-> -. suc A e. B ) )
17	16	con4bid	|- ( ( Ord B /\ Ord A ) -> ( A e. U. B <-> suc A e. B ) )
18	17	ex	|- ( Ord B -> ( Ord A -> ( A e. U. B <-> suc A e. B ) ) )
19	4 8 18	pm5.21ndd	|- ( Ord B -> ( A e. U. B <-> suc A e. B ) )