Metamath Proof Explorer

Theorem rankval4b

Description: The rank of a set is the supremum of the successors of the ranks of its members. Exercise 9.1 of Jech p. 72. Also a special case of Theorem 7V(b) of Enderton p. 204. This variant of rankval4 does not use Regularity, and so requires the assumption that A is in the range of R1 . (Contributed by BTernaryTau, 19-Jan-2026)

Ref Expression
Assertion rankval4b 
|- ( A e. U. ( R1 " On ) -> ( rank ` A ) = U_ x e. A suc ( rank ` x ) )

Proof

Step Hyp Ref Expression
1 r1wf 
 |-  ( R1 ` U_ x e. A suc ( rank ` x ) ) e. U. ( R1 " On )
2 rankon 
 |-  ( rank ` x ) e. On
3 2 onsuci 
 |-  suc ( rank ` x ) e. On
4 3 rgenw 
 |-  A. x e. A suc ( rank ` x ) e. On
5 iunon 
 |-  ( ( A e. U. ( R1 " On ) /\ A. x e. A suc ( rank ` x ) e. On ) -> U_ x e. A suc ( rank ` x ) e. On )
6 4 5 mpan2 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A suc ( rank ` x ) e. On )
7 r1ord3 
 |-  ( ( suc ( rank ` x ) e. On /\ U_ x e. A suc ( rank ` x ) e. On ) -> ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
8 3 6 7 sylancr 
 |-  ( A e. U. ( R1 " On ) -> ( suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
9 ssiun2 
 |-  ( x e. A -> suc ( rank ` x ) C_ U_ x e. A suc ( rank ` x ) )
10 8 9 impel 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> ( R1 ` suc ( rank ` x ) ) C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) )
11 elwf 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> x e. U. ( R1 " On ) )
12 rankidb 
 |-  ( x e. U. ( R1 " On ) -> x e. ( R1 ` suc ( rank ` x ) ) )
13 11 12 syl 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> x e. ( R1 ` suc ( rank ` x ) ) )
14 10 13 sseldd 
 |-  ( ( A e. U. ( R1 " On ) /\ x e. A ) -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) )
15 14 ex 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
16 15 alrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. x ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
17 nfcv 
 |-  F/_ x A
18 nfcv 
 |-  F/_ x R1
19 nfiu1 
 |-  F/_ x U_ x e. A suc ( rank ` x )
20 18 19 nffv 
 |-  F/_ x ( R1 ` U_ x e. A suc ( rank ` x ) )
21 17 20 dfssf 
 |-  ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) <-> A. x ( x e. A -> x e. ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
22 16 21 sylibr 
 |-  ( A e. U. ( R1 " On ) -> A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) )
23 rankssb 
 |-  ( ( R1 ` U_ x e. A suc ( rank ` x ) ) e. U. ( R1 " On ) -> ( A C_ ( R1 ` U_ x e. A suc ( rank ` x ) ) -> ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) ) )
24 1 22 23 mpsyl 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) )
25 r1ord3 
 |-  ( ( U_ x e. A suc ( rank ` x ) e. On /\ y e. On ) -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) )
26 6 25 sylan 
 |-  ( ( A e. U. ( R1 " On ) /\ y e. On ) -> ( U_ x e. A suc ( rank ` x ) C_ y -> ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) ) )
27 26 ss2rabdv 
 |-  ( A e. U. ( R1 " On ) -> { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } )
28 intss 
 |-  ( { y e. On | U_ x e. A suc ( rank ` x ) C_ y } C_ { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } -> |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } )
29 27 28 syl 
 |-  ( A e. U. ( R1 " On ) -> |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } C_ |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } )
30 rankval2b 
 |-  ( ( R1 ` U_ x e. A suc ( rank ` x ) ) e. U. ( R1 " On ) -> ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } )
31 1 30 mp1i 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) = |^| { y e. On | ( R1 ` U_ x e. A suc ( rank ` x ) ) C_ ( R1 ` y ) } )
32 intmin 
 |-  ( U_ x e. A suc ( rank ` x ) e. On -> |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x ) )
33 6 32 syl 
 |-  ( A e. U. ( R1 " On ) -> |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } = U_ x e. A suc ( rank ` x ) )
34 33 eqcomd 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A suc ( rank ` x ) = |^| { y e. On | U_ x e. A suc ( rank ` x ) C_ y } )
35 29 31 34 3sstr4d 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` ( R1 ` U_ x e. A suc ( rank ` x ) ) ) C_ U_ x e. A suc ( rank ` x ) )
36 24 35 sstrd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) C_ U_ x e. A suc ( rank ` x ) )
37 rankelb 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> ( rank ` x ) e. ( rank ` A ) ) )
38 rankon 
 |-  ( rank ` A ) e. On
39 2 38 onsucssi 
 |-  ( ( rank ` x ) e. ( rank ` A ) <-> suc ( rank ` x ) C_ ( rank ` A ) )
40 37 39 imbitrdi 
 |-  ( A e. U. ( R1 " On ) -> ( x e. A -> suc ( rank ` x ) C_ ( rank ` A ) ) )
41 40 ralrimiv 
 |-  ( A e. U. ( R1 " On ) -> A. x e. A suc ( rank ` x ) C_ ( rank ` A ) )
42 iunss 
 |-  ( U_ x e. A suc ( rank ` x ) C_ ( rank ` A ) <-> A. x e. A suc ( rank ` x ) C_ ( rank ` A ) )
43 41 42 sylibr 
 |-  ( A e. U. ( R1 " On ) -> U_ x e. A suc ( rank ` x ) C_ ( rank ` A ) )
44 36 43 eqssd 
 |-  ( A e. U. ( R1 " On ) -> ( rank ` A ) = U_ x e. A suc ( rank ` x ) )