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 𝐵 → ( 𝐴 ∈ 𝐵 ↔ suc 𝐴 ∈ suc 𝐵 ) )

Proof

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