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	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
	werankwe.2	⊢ ( 𝑤 = ( rank ‘ 𝑥 ) → 𝑇 = 𝑅 )
	werankwe.3	⊢ ( 𝑣 = 𝑥 → 𝑈 = 𝑅 )
Assertion	werankwe	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } → 𝑆 We 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		werankwe.1	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
2		werankwe.2	⊢ ( 𝑤 = ( rank ‘ 𝑥 ) → 𝑇 = 𝑅 )
3		werankwe.3	⊢ ( 𝑣 = 𝑥 → 𝑈 = 𝑅 )
4		fveq2	⊢ ( 𝑣 = 𝑥 → ( rank ‘ 𝑣 ) = ( rank ‘ 𝑥 ) )
5	4	eqeq2d	⊢ ( 𝑣 = 𝑥 → ( ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) ↔ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) ) )
6	5	rabbidv	⊢ ( 𝑣 = 𝑥 → { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } = { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } )
7	3 6	weeq12d	⊢ ( 𝑣 = 𝑥 → ( 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } ↔ 𝑅 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } ) )
8	7	cbvralvw	⊢ ( ∀ 𝑣 ∈ 𝐴 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } ↔ ∀ 𝑥 ∈ 𝐴 𝑅 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } )
9		fvex	⊢ ( rank ‘ 𝑦 ) ∈ V
10	9	epeli	⊢ ( ( rank ‘ 𝑥 ) E ( rank ‘ 𝑦 ) ↔ ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) )
11	10	orbi1i	⊢ ( ( ( rank ‘ 𝑥 ) E ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) ↔ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) )
12	11	opabbii	⊢ { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) E ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) } = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) ∈ ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
13	1 12	eqtr4i	⊢ 𝑆 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( ( rank ‘ 𝑥 ) E ( rank ‘ 𝑦 ) ∨ ( ( rank ‘ 𝑥 ) = ( rank ‘ 𝑦 ) ∧ 𝑥 𝑅 𝑦 ) ) }
14		fveqeq2	⊢ ( 𝑧 = 𝑦 → ( ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) ↔ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑥 ) ) )
15	14	cbvrabv	⊢ { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } = { 𝑦 ∈ 𝐴 ∣ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑥 ) }
16	6 15	eqtrdi	⊢ ( 𝑣 = 𝑥 → { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } = { 𝑦 ∈ 𝐴 ∣ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑥 ) } )
17	3 16	weeq12d	⊢ ( 𝑣 = 𝑥 → ( 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } ↔ 𝑅 We { 𝑦 ∈ 𝐴 ∣ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑥 ) } ) )
18	17	rspccva	⊢ ( ( ∀ 𝑣 ∈ 𝐴 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } ∧ 𝑥 ∈ 𝐴 ) → 𝑅 We { 𝑦 ∈ 𝐴 ∣ ( rank ‘ 𝑦 ) = ( rank ‘ 𝑥 ) } )
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	⊢ 𝐴 ⊆ V
23		fssres	⊢ ( ( rank : V ⟶ On ∧ 𝐴 ⊆ V ) → ( rank ↾ 𝐴 ) : 𝐴 ⟶ On )
24	21 22 23	mp2an	⊢ ( rank ↾ 𝐴 ) : 𝐴 ⟶ On
25	24	a1i	⊢ ( ∀ 𝑣 ∈ 𝐴 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } → ( rank ↾ 𝐴 ) : 𝐴 ⟶ On )
26		epweon	⊢ E We On
27	26	a1i	⊢ ( ∀ 𝑣 ∈ 𝐴 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } → E We On )
28	2 13 18 25 27	fnwe2	⊢ ( ∀ 𝑣 ∈ 𝐴 𝑈 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑣 ) } → 𝑆 We 𝐴 )
29	8 28	sylbir	⊢ ( ∀ 𝑥 ∈ 𝐴 𝑅 We { 𝑧 ∈ 𝐴 ∣ ( rank ‘ 𝑧 ) = ( rank ‘ 𝑥 ) } → 𝑆 We 𝐴 )