Theorem werankwe

Description: Construct a well-order given a relation R ( x ) that well-orders elements of the same rank. (Contributed by BTernaryTau, 16-Sep-2026)

	Ref	Expression
Hypotheses	werankwe.1	|- S = { <. x , y >. | ( ( rank ` x ) e. ( rank ` y ) \/ ( ( rank ` x ) = ( rank ` y ) /\ x R y ) ) }
	werankwe.2	|- ( w = ( rank ` x ) -> T = R )
	werankwe.3	|- ( v = x -> U = R )
Assertion	werankwe	|- ( A. x e. A R We { z e. A | ( rank ` z ) = ( rank ` x ) } -> S We A )

Proof

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