Metamath Proof Explorer

Theorem kardex

Description: The collection of all sets equinumerous to a set A and having the least possible rank is a set. This is the part of the justification of the definition of kard of Enderton p. 222. (Contributed by NM, 14-Dec-2003)

Ref Expression
Assertion kardex 
|- { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V

Proof

Step Hyp Ref Expression
1 df-rab 
 |-  { x e. { z | z ~~ A } | A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) } = { x | ( x e. { z | z ~~ A } /\ A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) ) }
2 vex 
 |-  x e. _V
3 breq1 
 |-  ( z = x -> ( z ~~ A <-> x ~~ A ) )
4 2 3 elab 
 |-  ( x e. { z | z ~~ A } <-> x ~~ A )
5 breq1 
 |-  ( z = y -> ( z ~~ A <-> y ~~ A ) )
6 5 ralab 
 |-  ( A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) <-> A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) )
7 4 6 anbi12i 
 |-  ( ( x e. { z | z ~~ A } /\ A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) ) <-> ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) )
8 7 abbii 
 |-  { x | ( x e. { z | z ~~ A } /\ A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) ) } = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) }
9 1 8 eqtri 
 |-  { x e. { z | z ~~ A } | A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) } = { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) }
10 scottex 
 |-  { x e. { z | z ~~ A } | A. y e. { z | z ~~ A } ( rank ` x ) C_ ( rank ` y ) } e. _V
11 9 10 eqeltrri 
 |-  { x | ( x ~~ A /\ A. y ( y ~~ A -> ( rank ` x ) C_ ( rank ` y ) ) ) } e. _V