This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )