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