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 onsuc 
 |-  ( 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 ax1w 
 |-  ( ( Ord A /\ x e. On ) -> ( suc x e. A -> ( x e. A -> suc x e. A ) ) )
17 15 16 jaod 
 |-  ( ( Ord A /\ x e. On ) -> ( ( A e. suc x \/ suc x e. A ) -> ( x e. A -> suc x e. A ) ) )
18 eloni 
 |-  ( x e. On -> Ord x )
19 ordtri2or 
 |-  ( ( Ord x /\ Ord A ) -> ( x e. A \/ A C_ x ) )
20 18 19 sylan 
 |-  ( ( x e. On /\ Ord A ) -> ( x e. A \/ A C_ x ) )
21 20 ancoms 
 |-  ( ( Ord A /\ x e. On ) -> ( x e. A \/ A C_ x ) )
22 21 orcomd 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x \/ x e. A ) )
23 22 adantr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A C_ x \/ x e. A ) )
24 ordsssuc2 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x <-> A e. suc x ) )
25 24 biimpd 
 |-  ( ( Ord A /\ x e. On ) -> ( A C_ x -> A e. suc x ) )
26 25 adantr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A C_ x -> A e. suc x ) )
27 simpr 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( x e. A -> suc x e. A ) )
28 26 27 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 ) ) )
29 23 28 mpd 
 |-  ( ( ( Ord A /\ x e. On ) /\ ( x e. A -> suc x e. A ) ) -> ( A e. suc x \/ suc x e. A ) )
30 29 ex 
 |-  ( ( Ord A /\ x e. On ) -> ( ( x e. A -> suc x e. A ) -> ( A e. suc x \/ suc x e. A ) ) )
31 17 30 impbid 
 |-  ( ( Ord A /\ x e. On ) -> ( ( A e. suc x \/ suc x e. A ) <-> ( x e. A -> suc x e. A ) ) )
32 8 31 bitr3d 
 |-  ( ( Ord A /\ x e. On ) -> ( -. A = suc x <-> ( x e. A -> suc x e. A ) ) )
33 32 pm5.74da 
 |-  ( Ord A -> ( ( x e. On -> -. A = suc x ) <-> ( x e. On -> ( x e. A -> suc x e. A ) ) ) )
34 impexp 
 |-  ( ( ( x e. On /\ x e. A ) -> suc x e. A ) <-> ( x e. On -> ( x e. A -> suc x e. A ) ) )
35 simpr 
 |-  ( ( x e. On /\ x e. A ) -> x e. A )
36 ordelon 
 |-  ( ( Ord A /\ x e. A ) -> x e. On )
37 36 ex 
 |-  ( Ord A -> ( x e. A -> x e. On ) )
38 37 ancrd 
 |-  ( Ord A -> ( x e. A -> ( x e. On /\ x e. A ) ) )
39 35 38 impbid2 
 |-  ( Ord A -> ( ( x e. On /\ x e. A ) <-> x e. A ) )
40 39 imbi1d 
 |-  ( Ord A -> ( ( ( x e. On /\ x e. A ) -> suc x e. A ) <-> ( x e. A -> suc x e. A ) ) )
41 34 40 bitr3id 
 |-  ( Ord A -> ( ( x e. On -> ( x e. A -> suc x e. A ) ) <-> ( x e. A -> suc x e. A ) ) )
42 33 41 bitrd 
 |-  ( Ord A -> ( ( x e. On -> -. A = suc x ) <-> ( x e. A -> suc x e. A ) ) )
43 42 ralbidv2 
 |-  ( Ord A -> ( A. x e. On -. A = suc x <-> A. x e. A suc x e. A ) )
44 2 43 bitr3id 
 |-  ( Ord A -> ( -. E. x e. On A = suc x <-> A. x e. A suc x e. A ) )
45 1 44 bitrd 
 |-  ( Ord A -> ( A = U. A <-> A. x e. A suc x e. A ) )