Metamath Proof Explorer

Theorem cardpred

Description: The cardinality function preserves predecessors. (Contributed by BTernaryTau, 18-Jul-2024)

Ref Expression
Assertion cardpred 
|- ( ( A C_ dom card /\ B e. dom card ) -> Pred ( _E , ( card " A ) , ( card ` B ) ) = ( card " Pred ( ~< , A , B ) ) )

Proof

Step Hyp Ref Expression
1 cardf2 
 |-  card : { x | E. y e. On y ~~ x } --> On
2 ffun 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> Fun card )
3 2 funfnd 
 |-  ( card : { x | E. y e. On y ~~ x } --> On -> card Fn dom card )
4 1 3 mp1i 
 |-  ( ( A C_ dom card /\ B e. dom card ) -> card Fn dom card )
5 fvex 
 |-  ( card ` y ) e. _V
6 5 epeli 
 |-  ( ( card ` x ) _E ( card ` y ) <-> ( card ` x ) e. ( card ` y ) )
7 cardsdom2 
 |-  ( ( x e. dom card /\ y e. dom card ) -> ( ( card ` x ) e. ( card ` y ) <-> x ~< y ) )
8 6 7 bitr2id 
 |-  ( ( x e. dom card /\ y e. dom card ) -> ( x ~< y <-> ( card ` x ) _E ( card ` y ) ) )
9 8 rgen2 
 |-  A. x e. dom card A. y e. dom card ( x ~< y <-> ( card ` x ) _E ( card ` y ) )
10 9 a1i 
 |-  ( ( A C_ dom card /\ B e. dom card ) -> A. x e. dom card A. y e. dom card ( x ~< y <-> ( card ` x ) _E ( card ` y ) ) )
11 simpl 
 |-  ( ( A C_ dom card /\ B e. dom card ) -> A C_ dom card )
12 simpr 
 |-  ( ( A C_ dom card /\ B e. dom card ) -> B e. dom card )
13 4 10 11 12 fnrelpredd 
 |-  ( ( A C_ dom card /\ B e. dom card ) -> Pred ( _E , ( card " A ) , ( card ` B ) ) = ( card " Pred ( ~< , A , B ) ) )