Metamath Proof Explorer

Theorem cardsdomel

Description: A cardinal strictly dominates its members. Equivalent to Proposition 10.37 of TakeutiZaring p. 93. (Contributed by Mario Carneiro, 15-Jan-2013) (Revised by Mario Carneiro, 4-Jun-2015)

Ref Expression
Assertion cardsdomel 
|- ( ( A e. On /\ B e. dom card ) -> ( A ~< B <-> A e. ( card ` B ) ) )

Proof

Step Hyp Ref Expression
1 cardid2 
 |-  ( B e. dom card -> ( card ` B ) ~~ B )
2 1 ensymd 
 |-  ( B e. dom card -> B ~~ ( card ` B ) )
3 sdomentr 
 |-  ( ( A ~< B /\ B ~~ ( card ` B ) ) -> A ~< ( card ` B ) )
4 2 3 sylan2 
 |-  ( ( A ~< B /\ B e. dom card ) -> A ~< ( card ` B ) )
5 ssdomg 
 |-  ( A e. On -> ( ( card ` B ) C_ A -> ( card ` B ) ~<_ A ) )
6 cardon 
 |-  ( card ` B ) e. On
7 domtriord 
 |-  ( ( ( card ` B ) e. On /\ A e. On ) -> ( ( card ` B ) ~<_ A <-> -. A ~< ( card ` B ) ) )
8 6 7 mpan 
 |-  ( A e. On -> ( ( card ` B ) ~<_ A <-> -. A ~< ( card ` B ) ) )
9 5 8 sylibd 
 |-  ( A e. On -> ( ( card ` B ) C_ A -> -. A ~< ( card ` B ) ) )
10 9 con2d 
 |-  ( A e. On -> ( A ~< ( card ` B ) -> -. ( card ` B ) C_ A ) )
11 ontri1 
 |-  ( ( ( card ` B ) e. On /\ A e. On ) -> ( ( card ` B ) C_ A <-> -. A e. ( card ` B ) ) )
12 6 11 mpan 
 |-  ( A e. On -> ( ( card ` B ) C_ A <-> -. A e. ( card ` B ) ) )
13 12 con2bid 
 |-  ( A e. On -> ( A e. ( card ` B ) <-> -. ( card ` B ) C_ A ) )
14 10 13 sylibrd 
 |-  ( A e. On -> ( A ~< ( card ` B ) -> A e. ( card ` B ) ) )
15 4 14 syl5 
 |-  ( A e. On -> ( ( A ~< B /\ B e. dom card ) -> A e. ( card ` B ) ) )
16 15 expcomd 
 |-  ( A e. On -> ( B e. dom card -> ( A ~< B -> A e. ( card ` B ) ) ) )
17 16 imp 
 |-  ( ( A e. On /\ B e. dom card ) -> ( A ~< B -> A e. ( card ` B ) ) )
18 cardsdomelir 
 |-  ( A e. ( card ` B ) -> A ~< B )
19 17 18 impbid1 
 |-  ( ( A e. On /\ B e. dom card ) -> ( A ~< B <-> A e. ( card ` B ) ) )