Metamath Proof Explorer


Theorem sucdomOLD

Description: Obsolete version of sucdom as of 4-Dec-2024. (Contributed by Mario Carneiro, 12-Jan-2013) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion sucdomOLD ( 𝐴 ∈ ω → ( 𝐴𝐵 ↔ suc 𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 sucdom2 ( 𝐴𝐵 → suc 𝐴𝐵 )
2 php4 ( 𝐴 ∈ ω → 𝐴 ≺ suc 𝐴 )
3 sdomdomtr ( ( 𝐴 ≺ suc 𝐴 ∧ suc 𝐴𝐵 ) → 𝐴𝐵 )
4 3 ex ( 𝐴 ≺ suc 𝐴 → ( suc 𝐴𝐵𝐴𝐵 ) )
5 2 4 syl ( 𝐴 ∈ ω → ( suc 𝐴𝐵𝐴𝐵 ) )
6 1 5 impbid2 ( 𝐴 ∈ ω → ( 𝐴𝐵 ↔ suc 𝐴𝐵 ) )