Metamath Proof Explorer

Theorem elkarden

Description: Any member of the kard cardinal number of a set is equinumerous to the set. Contrast with cardne for card cardinals. (Contributed by BTernaryTau, 3-Jul-2026)

Ref Expression
Assertion elkarden 
|- ( A e. ( kard ` B ) -> A ~~ B )

Proof

Step Hyp Ref Expression
1 breq1 
 |-  ( x = A -> ( x ~~ B <-> A ~~ B ) )
2 fveq2 
 |-  ( x = A -> ( rank ` x ) = ( rank ` A ) )
3 2 sseq1d 
 |-  ( x = A -> ( ( rank ` x ) C_ ( rank ` y ) <-> ( rank ` A ) C_ ( rank ` y ) ) )
4 3 imbi2d 
 |-  ( x = A -> ( ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) <-> ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) )
5 4 albidv 
 |-  ( x = A -> ( A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) <-> A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) )
6 1 5 anbi12d 
 |-  ( x = A -> ( ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) <-> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) )
7 kardval2 
 |-  ( kard ` B ) = { x | ( x ~~ B /\ A. y ( y ~~ B -> ( rank ` x ) C_ ( rank ` y ) ) ) }
8 6 7 elab2g 
 |-  ( A e. ( kard ` B ) -> ( A e. ( kard ` B ) <-> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) ) )
9 8 ibi 
 |-  ( A e. ( kard ` B ) -> ( A ~~ B /\ A. y ( y ~~ B -> ( rank ` A ) C_ ( rank ` y ) ) ) )
10 9 simpld 
 |-  ( A e. ( kard ` B ) -> A ~~ B )