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∈B↔suc⁡A∈suc⁡B

Proof

Step Hyp Ref Expression
1 simpl ⊢Ord⁡B∧A∈B→Ord⁡B
2 ordelord ⊢Ord⁡B∧A∈B→Ord⁡A
3 1 2 jca ⊢Ord⁡B∧A∈B→Ord⁡B∧Ord⁡A
4 simpl ⊢Ord⁡B∧suc⁡A∈suc⁡B→Ord⁡B
5 ordsuc ⊢Ord⁡B↔Ord⁡suc⁡B
6 ordelord ⊢Ord⁡suc⁡B∧suc⁡A∈suc⁡B→Ord⁡suc⁡A
7 ordsuc ⊢Ord⁡A↔Ord⁡suc⁡A
8 6 7 sylibr ⊢Ord⁡suc⁡B∧suc⁡A∈suc⁡B→Ord⁡A
9 5 8 sylanb ⊢Ord⁡B∧suc⁡A∈suc⁡B→Ord⁡A
10 4 9 jca ⊢Ord⁡B∧suc⁡A∈suc⁡B→Ord⁡B∧Ord⁡A
11 ordsseleq ⊢Ord⁡suc⁡A∧Ord⁡B→suc⁡A⊆B↔suc⁡A∈B∨suc⁡A=B
12 7 11 sylanb ⊢Ord⁡A∧Ord⁡B→suc⁡A⊆B↔suc⁡A∈B∨suc⁡A=B
13 12 ancoms ⊢Ord⁡B∧Ord⁡A→suc⁡A⊆B↔suc⁡A∈B∨suc⁡A=B
14 13 adantl ⊢A∈V∧Ord⁡B∧Ord⁡A→suc⁡A⊆B↔suc⁡A∈B∨suc⁡A=B
15 ordsucss ⊢Ord⁡B→A∈B→suc⁡A⊆B
16 15 ad2antrl ⊢A∈V∧Ord⁡B∧Ord⁡A→A∈B→suc⁡A⊆B
17 sucssel ⊢A∈V→suc⁡A⊆B→A∈B
18 17 adantr ⊢A∈V∧Ord⁡B∧Ord⁡A→suc⁡A⊆B→A∈B
19 16 18 impbid ⊢A∈V∧Ord⁡B∧Ord⁡A→A∈B↔suc⁡A⊆B
20 sucexb ⊢A∈V↔suc⁡A∈V
21 elsucg ⊢suc⁡A∈V→suc⁡A∈suc⁡B↔suc⁡A∈B∨suc⁡A=B
22 20 21 sylbi ⊢A∈V→suc⁡A∈suc⁡B↔suc⁡A∈B∨suc⁡A=B
23 22 adantr ⊢A∈V∧Ord⁡B∧Ord⁡A→suc⁡A∈suc⁡B↔suc⁡A∈B∨suc⁡A=B
24 14 19 23 3bitr4d ⊢A∈V∧Ord⁡B∧Ord⁡A→A∈B↔suc⁡A∈suc⁡B
25 24 ex ⊢A∈V→Ord⁡B∧Ord⁡A→A∈B↔suc⁡A∈suc⁡B
26 elex ⊢A∈B→A∈V
27 elex ⊢suc⁡A∈suc⁡B→suc⁡A∈V
28 27 20 sylibr ⊢suc⁡A∈suc⁡B→A∈V
29 26 28 pm5.21ni ⊢¬A∈V→A∈B↔suc⁡A∈suc⁡B
30 29 a1d ⊢¬A∈V→Ord⁡B∧Ord⁡A→A∈B↔suc⁡A∈suc⁡B
31 25 30 pm2.61i ⊢Ord⁡B∧Ord⁡A→A∈B↔suc⁡A∈suc⁡B
32 3 10 31 pm5.21nd ⊢Ord⁡B→A∈B↔suc⁡A∈suc⁡B