Theorem cardsdomelir

Description: A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of TakeutiZaring p. 93. This is half of the assertion cardsdomel and can be proven without the AC. (Contributed by Mario Carneiro, 15-Jan-2013)

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

Proof

Step	Hyp	Ref	Expression
1		cardon	⊢ ( card ‘ 𝐵 ) ∈ On
2	1	onelssi	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ⊆ ( card ‘ 𝐵 ) )
3		ssdomg	⊢ ( ( card ‘ 𝐵 ) ∈ On → ( 𝐴 ⊆ ( card ‘ 𝐵 ) → 𝐴 ≼ ( card ‘ 𝐵 ) ) )
4	1 2 3	mpsyl	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ≼ ( card ‘ 𝐵 ) )
5		elfvdm	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐵 ∈ dom card )
6		cardid2	⊢ ( 𝐵 ∈ dom card → ( card ‘ 𝐵 ) ≈ 𝐵 )
7	5 6	syl	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ( card ‘ 𝐵 ) ≈ 𝐵 )
8		domentr	⊢ ( ( 𝐴 ≼ ( card ‘ 𝐵 ) ∧ ( card ‘ 𝐵 ) ≈ 𝐵 ) → 𝐴 ≼ 𝐵 )
9	4 7 8	syl2anc	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ≼ 𝐵 )
10		cardne	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → ¬ 𝐴 ≈ 𝐵 )
11		brsdom	⊢ ( 𝐴 ≺ 𝐵 ↔ ( 𝐴 ≼ 𝐵 ∧ ¬ 𝐴 ≈ 𝐵 ) )
12	9 10 11	sylanbrc	⊢ ( 𝐴 ∈ ( card ‘ 𝐵 ) → 𝐴 ≺ 𝐵 )