Metamath Proof Explorer


Theorem ssctOLD

Description: Obsolete version of ssct as of 7-Dec-2024. (Contributed by Thierry Arnoux, 31-Jan-2017) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion ssctOLD ( ( 𝐴𝐵𝐵 ≼ ω ) → 𝐴 ≼ ω )

Proof

Step Hyp Ref Expression
1 ctex ( 𝐵 ≼ ω → 𝐵 ∈ V )
2 ssdomg ( 𝐵 ∈ V → ( 𝐴𝐵𝐴𝐵 ) )
3 1 2 syl ( 𝐵 ≼ ω → ( 𝐴𝐵𝐴𝐵 ) )
4 3 impcom ( ( 𝐴𝐵𝐵 ≼ ω ) → 𝐴𝐵 )
5 domtr ( ( 𝐴𝐵𝐵 ≼ ω ) → 𝐴 ≼ ω )
6 4 5 sylancom ( ( 𝐴𝐵𝐵 ≼ ω ) → 𝐴 ≼ ω )