Theorem sdomsdomcard

Description: A set strictly dominates iff its cardinal strictly dominates. (Contributed by NM, 30-Oct-2003)

	Ref	Expression
Assertion	sdomsdomcard	⊢ ( 𝐴 ≺ 𝐵 ↔ 𝐴 ≺ ( card ‘ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		relsdom	⊢ Rel ≺
2	1	brrelex2i	⊢ ( 𝐴 ≺ 𝐵 → 𝐵 ∈ V )
3		numth3	⊢ ( 𝐵 ∈ V → 𝐵 ∈ dom card )
4		cardid2	⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
5		ensym	⊢ ( ( card ‘ 𝐵 ) ≈ 𝐵 → 𝐵 ≈ ( card ‘ 𝐵 ) )
6	2 3 4 5	4syl	⊢ ( 𝐴 ≺ 𝐵 → 𝐵 ≈ ( card ‘ 𝐵 ) )
7		sdomentr	⊢ ( ( 𝐴 ≺ 𝐵 ∧ 𝐵 ≈ ( card ‘ 𝐵 ) ) → 𝐴 ≺ ( card ‘ 𝐵 ) )
8	6 7	mpdan	⊢ ( 𝐴 ≺ 𝐵 → 𝐴 ≺ ( card ‘ 𝐵 ) )
9		sdomsdomcardi	⊢ ( 𝐴 ≺ ( card ‘ 𝐵 ) → 𝐴 ≺ 𝐵 )
10	8 9	impbii	⊢ ( 𝐴 ≺ 𝐵 ↔ 𝐴 ≺ ( card ‘ 𝐵 ) )