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

Proof

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