Metamath Proof Explorer

Theorem rankse

Description: Construct a relation that is set-like on any class. (Contributed by BTernaryTau, 18-Sep-2026)

Ref Expression
Hypothesis rankse.1 
|- S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) }
Assertion rankse 
|- S Se A

Proof

Step Hyp Ref Expression
1 rankse.1 
 |-  S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) }
2 rankon 
 |-  ( rank ` y ) e. On
3 id 
 |-  ( ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) )
4 3 rgenw 
 |-  A. x e. A ( ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) )
5 fveq2 
 |-  ( v = x -> ( rank ` v ) = ( rank ` x ) )
6 5 sseq1d 
 |-  ( v = x -> ( ( rank ` v ) C_ ( rank ` y ) <-> ( rank ` x ) C_ ( rank ` y ) ) )
7 6 ralrab2 
 |-  ( A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ ( rank ` y ) <-> A. x e. A ( ( rank ` x ) C_ ( rank ` y ) -> ( rank ` x ) C_ ( rank ` y ) ) )
8 4 7 mpbir 
 |-  A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ ( rank ` y )
9 sseq2 
 |-  ( u = ( rank ` y ) -> ( ( rank ` v ) C_ u <-> ( rank ` v ) C_ ( rank ` y ) ) )
10 9 ralbidv 
 |-  ( u = ( rank ` y ) -> ( A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ u <-> A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ ( rank ` y ) ) )
11 10 rspcev 
 |-  ( ( ( rank ` y ) e. On /\ A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ ( rank ` y ) ) -> E. u e. On A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ u )
12 2 8 11 mp2an 
 |-  E. u e. On A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ u
13 bndrank 
 |-  ( E. u e. On A. v e. { x e. A | ( rank ` x ) C_ ( rank ` y ) } ( rank ` v ) C_ u -> { x e. A | ( rank ` x ) C_ ( rank ` y ) } e. _V )
14 12 13 ax-mp 
 |-  { x e. A | ( rank ` x ) C_ ( rank ` y ) } e. _V
15 simpl 
 |-  ( ( ( rank ` x ) = ( rank ` y ) /\ ph ) -> ( rank ` x ) = ( rank ` y ) )
16 15 orim2i 
 |-  ( ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) -> ( ( rank ` x ) e. ( rank ` y ) \/ ( rank ` x ) = ( rank ` y ) ) )
17 1 breqi 
 |-  ( x S y <-> x { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) } y )
18 df-br 
 |-  ( x { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) } y <-> <. x , y >. e. { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) } )
19 opabidw 
 |-  ( <. x , y >. e. { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) } <-> ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) )
20 17 18 19 3bitri 
 |-  ( x S y <-> ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) )
21 rankon 
 |-  ( rank ` x ) e. On
22 21 2 onsseli 
 |-  ( ( rank ` x ) C_ ( rank ` y ) <-> ( ( rank ` x ) e. ( rank ` y ) \/ ( rank ` x ) = ( rank ` y ) ) )
23 16 20 22 3imtr4i 
 |-  ( x S y -> ( rank ` x ) C_ ( rank ` y ) )
24 23 a1i 
 |-  ( x e. A -> ( x S y -> ( rank ` x ) C_ ( rank ` y ) ) )
25 24 ss2rabi 
 |-  { x e. A | x S y } C_ { x e. A | ( rank ` x ) C_ ( rank ` y ) }
26 14 25 ssexi 
 |-  { x e. A | x S y } e. _V
27 26 rgenw 
 |-  A. y e. A { x e. A | x S y } e. _V
28 nfcv 
 |-  F/_ x A
29 nfcv 
 |-  F/_ z A
30 nfv 
 |-  F/ z x S w
31 nfcv 
 |-  F/_ x z
32 nfopab1 
 |-  F/_ x { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) }
33 1 32 nfcxfr 
 |-  F/_ x S
34 nfcv 
 |-  F/_ x w
35 31 33 34 nfbr 
 |-  F/ x z S w
36 breq1 
 |-  ( x = z -> ( x S w <-> z S w ) )
37 28 29 30 35 36 cbvrabw 
 |-  { x e. A | x S w } = { z e. A | z S w }
38 37 eleq1i 
 |-  ( { x e. A | x S w } e. _V <-> { z e. A | z S w } e. _V )
39 38 ralbii 
 |-  ( A. w e. A { x e. A | x S w } e. _V <-> A. w e. A { z e. A | z S w } e. _V )
40 nfv 
 |-  F/ w { x e. A | x S y } e. _V
41 nfcv 
 |-  F/_ y x
42 nfopab2 
 |-  F/_ y { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ ph ) ) }
43 1 42 nfcxfr 
 |-  F/_ y S
44 nfcv 
 |-  F/_ y w
45 41 43 44 nfbr 
 |-  F/ y x S w
46 nfcv 
 |-  F/_ y A
47 45 46 nfrabw 
 |-  F/_ y { x e. A | x S w }
48 47 nfel1 
 |-  F/ y { x e. A | x S w } e. _V
49 breq2 
 |-  ( y = w -> ( x S y <-> x S w ) )
50 49 rabbidv 
 |-  ( y = w -> { x e. A | x S y } = { x e. A | x S w } )
51 50 eleq1d 
 |-  ( y = w -> ( { x e. A | x S y } e. _V <-> { x e. A | x S w } e. _V ) )
52 40 48 51 cbvralw 
 |-  ( A. y e. A { x e. A | x S y } e. _V <-> A. w e. A { x e. A | x S w } e. _V )
53 df-se 
 |-  ( S Se A <-> A. w e. A { z e. A | z S w } e. _V )
54 39 52 53 3bitr4ri 
 |-  ( S Se A <-> A. y e. A { x e. A | x S y } e. _V )
55 27 54 mpbir 
 |-  S Se A