Metamath Proof Explorer

Theorem ordunisuc2

Description: An ordinal equal to its union contains the successor of each of its members. (Contributed by NM, 1-Feb-2005)

Ref Expression
Assertion ordunisuc2 
|- ( Ord A -> ( A = U. A <-> A. x e. A suc x e. A ) )

Proof

Step Hyp Ref Expression
1 orduninsuc 
 |-  ( Ord A -> ( A = U. A <-> -. E. x e. On A = suc x ) )
2 ralnex 
 |-  ( A. x e. On -. A = suc x <-> -. E. x e. On A = suc x )
3 suceloni 
 |-  ( x e. On -> suc x e. On )
4 eloni 
 |-  ( suc x e. On -> Ord suc x )
5 3 4 syl 
 |-  ( x e. On -> Ord suc x )
6 ordtri3 
 |-  ( ( Ord A /\ Ord suc x ) -> ( A = suc x <-> -. ( A e. suc x \/ suc x e. A ) ) )
7 5 6 sylan2 
 |-  ( ( Ord A /\ x e. On ) -> ( A = suc x <-> -. ( A e. suc x \/ suc x e. A ) ) )
8 7 con2bid 
 |-  ( ( Ord A /\ x e. On ) -> ( ( A e. suc x \/ suc x e. A ) <-> -. A = suc x ) )
9 onnbtwn 
 |-  ( x e. On -> -. ( x e. A /\ A e. suc x ) )
10 imnan 
 |-  ( ( x e. A -> -. A e. suc x ) <-> -. ( x e. A /\ A e. suc x ) )
11 9 10 sylibr 
 |-  ( x e. On -> ( x e. A -> -. A e. suc x ) )
12 11 con2d 
 |-  ( x e. On -> ( A e. suc x -> -. x e. A ) )
13 pm2.21 
 |-  ( -. x e. A -> ( x e. A -> suc x e. A ) )
14 12 13 syl6 
 |-  ( x e. On -> ( A e. suc x -> ( x e. A -> suc x e. A ) ) )
15 14 adantl 
 |-  ( ( Ord A /\ x e. On ) -> ( A e. suc x -> ( x e. A -> suc x e. A ) ) )
16 ax-1 
 |-  ( suc x e. A -> ( x e. A -> suc x e. A ) )
17 16 a1i 
 |-  ( ( Ord A /\ x e. On ) -> ( suc x e. A -> ( x e. A -> suc x e. A ) ) )
18 15 17 jaod 
 |-  ( ( Ord A /\ x e. On ) -> ( ( A e. suc x \/ suc x e. A ) -> ( x e. A -> suc x e. A ) ) )
19 eloni 
 |-  ( x e. On -> Ord x )
20 ordtri2or 
 |-  ( ( Ord x /\ Ord A ) -> ( x e. A \/ A C_ x ) )
21 19 20 sylan 
 |-  ( ( x e. On /\ Ord A ) -> ( x e. A \/ A C_ x ) )
22 21 ancoms 
 |-  ( ( Ord A /\ x e. On ) -> ( x e. A \/ A C_ x ) )
23 22 orcomd 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x \/ x e. A ) )
24 23 adantr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A C_ x \/ x e. A ) )
25 ordsssuc2 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x <-> A e. suc x ) )
26 25 biimpd 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x -> A e. suc x ) )
27 26 adantr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A C_ x -> A e. suc x ) )
28 simpr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( x e. A -> suc x e. A ) )
29 27 28 orim12d 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( ( A C_ x \/ x e. A ) -> ( A e. suc x \/ suc x e. A ) ) )
30 24 29 mpd 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A e. suc x \/ suc x e. A ) )
31 30 ex 
 |-  ( ( Ord A /\ x e. On ) -> ( ( x e. A -> suc x e. A ) -> ( A e. suc x \/ suc x e. A ) ) )
32 18 31 impbid 
 |-  ( ( Ord A /\ x e. On ) -> ( ( A e. suc x \/ suc x e. A ) <-> ( x e. A -> suc x e. A ) ) )
33 8 32 bitr3d 
 |-  ( ( Ord A /\ x e. On ) -> ( -. A = suc x <-> ( x e. A -> suc x e. A ) ) )
34 33 pm5.74da 
 |-  ( Ord A -> ( ( x e. On -> -. A = suc x ) <-> ( x e. On -> ( x e. A -> suc x e. A ) ) ) )
35 impexp 
 |-  ( ( ( x e. On /\ x e. A ) -> suc x e. A ) <-> ( x e. On -> ( x e. A -> suc x e. A ) ) )
36 simpr 
 |-  ( ( x e. On /\ x e. A ) -> x e. A )
37 ordelon 
 |-  ( ( Ord A /\ x e. A ) -> x e. On )
38 37 ex 
 |-  ( Ord A -> ( x e. A -> x e. On ) )
39 38 ancrd 
 |-  ( Ord A -> ( x e. A -> ( x e. On /\ x e. A ) ) )
40 36 39 impbid2 
 |-  ( Ord A -> ( ( x e. On /\ x e. A ) <-> x e. A ) )
41 40 imbi1d 
 |-  ( Ord A -> ( ( ( x e. On /\ x e. A ) -> suc x e. A ) <-> ( x e. A -> suc x e. A ) ) )
42 35 41 bitr3id 
 |-  ( Ord A -> ( ( x e. On -> ( x e. A -> suc x e. A ) ) <-> ( x e. A -> suc x e. A ) ) )
43 34 42 bitrd 
 |-  ( Ord A -> ( ( x e. On -> -. A = suc x ) <-> ( x e. A -> suc x e. A ) ) )
44 43 ralbidv2 
 |-  ( Ord A -> ( A. x e. On -. A = suc x <-> A. x e. A suc x e. A ) )
45 2 44 bitr3id 
 |-  ( Ord A -> ( -. E. x e. On A = suc x <-> A. x e. A suc x e. A ) )
46 1 45 bitrd 
 |-  ( Ord A -> ( A = U. A <-> A. x e. A suc x e. A ) )