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