Theorem sdomsdomcardi

Description: A set strictly dominates if its cardinal strictly dominates. (Contributed by Mario Carneiro, 13-Jan-2013)

	Ref	Expression
Assertion	sdomsdomcardi	⊢ ( 𝐴 ≺ ( card ‘ 𝐵 ) → 𝐴 ≺ 𝐵 )

Proof

Step	Hyp	Ref	Expression
1		sdom0	⊢ ¬ 𝐴 ≺ ∅
2		ndmfv	⊢ ( ¬ 𝐵 ∈ dom card → ( card ‘ 𝐵 ) = ∅ )
3	2	breq2d	⊢ ( ¬ 𝐵 ∈ dom card → ( 𝐴 ≺ ( card ‘ 𝐵 ) ↔ 𝐴 ≺ ∅ ) )
4	1 3	mtbiri	⊢ ( ¬ 𝐵 ∈ dom card → ¬ 𝐴 ≺ ( card ‘ 𝐵 ) )
5	4	con4i	⊢ ( 𝐴 ≺ ( card ‘ 𝐵 ) → 𝐵 ∈ dom card )
6		cardid2	⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
7	5 6	syl	⊢ ( 𝐴 ≺ ( card ‘ 𝐵 ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
8		sdomentr	⊢ ( ( 𝐴 ≺ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → 𝐴 ≺ 𝐵 )
9	7 8	mpdan	⊢ ( 𝐴 ≺ ( card ‘ 𝐵 ) → 𝐴 ≺ 𝐵 )