Metamath Proof Explorer

Theorem werankwe2

Description: Construct a well-order given a relation that well-orders elements of the same rank. See werankwe for a version where R can depend on w . (Contributed by BTernaryTau, 18-Sep-2026)

Ref Expression
Hypothesis werankwe2.1 
|- S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
Assertion werankwe2 
|- ( A. w e. A R We { z e. A | ( rank ` z ) = ( rank ` w ) } -> S We A )

Proof

Step Hyp Ref Expression
1 werankwe2.1 
 |-  S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
2 eqidd 
 |-  ( v = ( rank ` x ) -> R = R )
3 fvex 
 |-  ( rank ` y ) e. _V
4 3 epeli 
 |-  ( ( rank ` x ) _E ( rank ` y ) <-> ( rank ` x ) e. ( rank ` y ) )
5 4 orbi1i 
 |-  ( ( ( rank ` x ) _E ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) <-> ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) )
6 5 opabbii 
 |-  { <. x , y >. | ( ( rank ` x ) _E ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) } = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
7 1 6 eqtr4i 
 |-  S = { <. x , y >. | ( ( rank ` x ) _E ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
8 eqidd 
 |-  ( w = x -> R = R )
9 fveq2 
 |-  ( w = x -> ( rank ` w ) = ( rank ` x ) )
10 9 eqeq2d 
 |-  ( w = x -> ( ( rank ` z ) = ( rank ` w ) <-> ( rank ` z ) = ( rank ` x ) ) )
11 10 rabbidv 
 |-  ( w = x -> { z e. A | ( rank ` z ) = ( rank ` w ) } = { z e. A | ( rank ` z ) = ( rank ` x ) } )
12 fveqeq2 
 |-  ( z = y -> ( ( rank ` z ) = ( rank ` x ) <-> ( rank ` y ) = ( rank ` x ) ) )
13 12 cbvrabv 
 |-  { z e. A | ( rank ` z ) = ( rank ` x ) } = { y e. A | ( rank ` y ) = ( rank ` x ) }
14 11 13 eqtrdi 
 |-  ( w = x -> { z e. A | ( rank ` z ) = ( rank ` w ) } = { y e. A | ( rank ` y ) = ( rank ` x ) } )
15 8 14 weeq12d 
 |-  ( w = x -> ( R We { z e. A | ( rank ` z ) = ( rank ` w ) } <-> R We { y e. A | ( rank ` y ) = ( rank ` x ) } ) )
16 15 rspccva 
 |-  ( ( A. w e. A R We { z e. A | ( rank ` z ) = ( rank ` w ) } /\ x e. A ) -> R We { y e. A | ( rank ` y ) = ( rank ` x ) } )
17 rankfo 
 |-  rank : _V -onto-> On
18 fof 
 |-  ( rank : _V -onto-> On -> rank : _V --> On )
19 17 18 ax-mp 
 |-  rank : _V --> On
20 ssv 
 |-  A C_ _V
21 fssres 
 |-  ( ( rank : _V --> On /\ A C_ _V ) -> ( rank |` A ) : A --> On )
22 19 20 21 mp2an 
 |-  ( rank |` A ) : A --> On
23 22 a1i 
 |-  ( A. w e. A R We { z e. A | ( rank ` z ) = ( rank ` w ) } -> ( rank |` A ) : A --> On )
24 epweon 
 |-  _E We On
25 24 a1i 
 |-  ( A. w e. A R We { z e. A | ( rank ` z ) = ( rank ` w ) } -> _E We On )
26 2 7 16 23 25 fnwe2 
 |-  ( A. w e. A R We { z e. A | ( rank ` z ) = ( rank ` w ) } -> S We A )