Metamath Proof Explorer


Theorem sdomel

Description: For ordinals, strict dominance implies membership. (Contributed by Mario Carneiro, 13-Jan-2013)

Ref Expression
Assertion sdomel ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴𝐵𝐴𝐵 ) )

Proof

Step Hyp Ref Expression
1 ssdomg ( 𝐴 ∈ On → ( 𝐵𝐴𝐵𝐴 ) )
2 1 adantl ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵𝐴𝐵𝐴 ) )
3 ontri1 ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵𝐴 ↔ ¬ 𝐴𝐵 ) )
4 domtriord ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐵𝐴 ↔ ¬ 𝐴𝐵 ) )
5 2 3 4 3imtr3d ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( ¬ 𝐴𝐵 → ¬ 𝐴𝐵 ) )
6 5 con4d ( ( 𝐵 ∈ On ∧ 𝐴 ∈ On ) → ( 𝐴𝐵𝐴𝐵 ) )
7 6 ancoms ( ( 𝐴 ∈ On ∧ 𝐵 ∈ On ) → ( 𝐴𝐵𝐴𝐵 ) )