Metamath Proof Explorer

Theorem ordsucelsuc

Description: Membership is inherited by successors. Generalization of Exercise 9 of TakeutiZaring p. 42. (Contributed by NM, 22-Jun-1998) (Proof shortened by Andrew Salmon, 12-Aug-2011)

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

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( Ord B /\ A e. B ) -> Ord B )
2 ordelord 
 |-  ( ( Ord B /\ A e. B ) -> Ord A )
3 1 2 jca 
 |-  ( ( Ord B /\ A e. B ) -> ( Ord B /\ Ord A ) )
4 simpl 
 |-  ( ( Ord B /\ suc A e. suc B ) -> Ord B )
5 ordsuc 
 |-  ( Ord B <-> Ord suc B )
6 ordelord 
 |-  ( ( Ord suc B /\ suc A e. suc B ) -> Ord suc A )
7 ordsuc 
 |-  ( Ord A <-> Ord suc A )
8 6 7 sylibr 
 |-  ( ( Ord suc B /\ suc A e. suc B ) -> Ord A )
9 5 8 sylanb 
 |-  ( ( Ord B /\ suc A e. suc B ) -> Ord A )
10 4 9 jca 
 |-  ( ( Ord B /\ suc A e. suc B ) -> ( Ord B /\ Ord A ) )
11 ordsseleq 
 |-  ( ( Ord suc A /\ Ord B ) -> ( suc A C_ B <-> ( suc A e. B \/ suc A = B ) ) )
12 7 11 sylanb 
 |-  ( ( Ord A /\ Ord B ) -> ( suc A C_ B <-> ( suc A e. B \/ suc A = B ) ) )
13 12 ancoms 
 |-  ( ( Ord B /\ Ord A ) -> ( suc A C_ B <-> ( suc A e. B \/ suc A = B ) ) )
14 13 adantl 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( suc A C_ B <-> ( suc A e. B \/ suc A = B ) ) )
15 ordsucss 
 |-  ( Ord B -> ( A e. B -> suc A C_ B ) )
16 15 ad2antrl 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( A e. B -> suc A C_ B ) )
17 sucssel 
 |-  ( A e. _V -> ( suc A C_ B -> A e. B ) )
18 17 adantr 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( suc A C_ B -> A e. B ) )
19 16 18 impbid 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( A e. B <-> suc A C_ B ) )
20 sucexb 
 |-  ( A e. _V <-> suc A e. _V )
21 elsucg 
 |-  ( suc A e. _V -> ( suc A e. suc B <-> ( suc A e. B \/ suc A = B ) ) )
22 20 21 sylbi 
 |-  ( A e. _V -> ( suc A e. suc B <-> ( suc A e. B \/ suc A = B ) ) )
23 22 adantr 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( suc A e. suc B <-> ( suc A e. B \/ suc A = B ) ) )
24 14 19 23 3bitr4d 
 |-  ( ( A e. _V /\ ( Ord B /\ Ord A ) ) -> ( A e. B <-> suc A e. suc B ) )
25 24 ex 
 |-  ( A e. _V -> ( ( Ord B /\ Ord A ) -> ( A e. B <-> suc A e. suc B ) ) )
26 elex 
 |-  ( A e. B -> A e. _V )
27 elex 
 |-  ( suc A e. suc B -> suc A e. _V )
28 27 20 sylibr 
 |-  ( suc A e. suc B -> A e. _V )
29 26 28 pm5.21ni 
 |-  ( -. A e. _V -> ( A e. B <-> suc A e. suc B ) )
30 29 a1d 
 |-  ( -. A e. _V -> ( ( Ord B /\ Ord A ) -> ( A e. B <-> suc A e. suc B ) ) )
31 25 30 pm2.61i 
 |-  ( ( Ord B /\ Ord A ) -> ( A e. B <-> suc A e. suc B ) )
32 3 10 31 pm5.21nd 
 |-  ( Ord B -> ( A e. B <-> suc A e. suc B ) )