Metamath Proof Explorer


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
|- ( A e. ( card ` B ) -> A ~< B )

Proof

Step Hyp Ref Expression
1 cardon
 |-  ( card ` B ) e. On
2 1 onelssi
 |-  ( A e. ( card ` B ) -> A C_ ( card ` B ) )
3 ssdomg
 |-  ( ( card ` B ) e. On -> ( A C_ ( card ` B ) -> A ~<_ ( card ` B ) ) )
4 1 2 3 mpsyl
 |-  ( A e. ( card ` B ) -> A ~<_ ( card ` B ) )
5 elfvdm
 |-  ( A e. ( card ` B ) -> B e. dom card )
6 cardid2
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
7 5 6 syl
 |-  ( A e. ( card ` B ) -> ( card ` B ) ~~ B )
8 domentr
 |-  ( ( A ~<_ ( card ` B ) /\ ( card ` B ) ~~ B ) -> A ~<_ B )
9 4 7 8 syl2anc
 |-  ( A e. ( card ` B ) -> A ~<_ B )
10 cardne
 |-  ( A e. ( card ` B ) -> -. A ~~ B )
11 brsdom
 |-  ( A ~< B <-> ( A ~<_ B /\ -. A ~~ B ) )
12 9 10 11 sylanbrc
 |-  ( A e. ( card ` B ) -> A ~< B )