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

Metamath Proof Explorer

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