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) \in rank (y) \lor (rank (x) = rank (y) \land x R y))\}$
	werankwe.2	$⊢ w = rank (x) \to T = R$
	werankwe.3	$⊢ v = x \to U = R$
Assertion	werankwe	$⊢ \forall x \in A R We \{z \in A \| rank (z) = rank (x)\} \to S We A$

Proof

Step	Hyp	Ref	Expression
1		werankwe.1	$⊢ S = \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land x R y))\}$
2		werankwe.2	$⊢ w = rank (x) \to T = R$
3		werankwe.3	$⊢ v = x \to U = R$
4		fveq2	$⊢ v = x \to rank (v) = rank (x)$
5	4	eqeq2d	$⊢ v = x \to (rank (z) = rank (v) \leftrightarrow rank (z) = rank (x))$
6	5	rabbidv	$⊢ v = x \to \{z \in A \| rank (z) = rank (v)\} = \{z \in A \| rank (z) = rank (x)\}$
7	3 6	weeq12d	$⊢ v = x \to (U We \{z \in A \| rank (z) = rank (v)\} \leftrightarrow R We \{z \in A \| rank (z) = rank (x)\})$
8	7	cbvralvw	$⊢ \forall v \in A U We \{z \in A \| rank (z) = rank (v)\} \leftrightarrow \forall x \in A R We \{z \in A \| rank (z) = rank (x)\}$
9		fvex	$⊢ rank (y) \in V$
10	9	epeli	$⊢ rank (x) E rank (y) \leftrightarrow rank (x) \in rank (y)$
11	10	orbi1i	$⊢ (rank (x) E rank (y) \lor (rank (x) = rank (y) \land x R y)) \leftrightarrow (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land x R y))$
12	11	opabbii	$⊢ \{⟨x, y⟩ \| (rank (x) E rank (y) \lor (rank (x) = rank (y) \land x R y))\} = \{⟨x, y⟩ \| (rank (x) \in rank (y) \lor (rank (x) = rank (y) \land x R y))\}$
13	1 12	eqtr4i	$⊢ S = \{⟨x, y⟩ \| (rank (x) E rank (y) \lor (rank (x) = rank (y) \land x R y))\}$
14		fveqeq2	$⊢ z = y \to (rank (z) = rank (x) \leftrightarrow rank (y) = rank (x))$
15	14	cbvrabv	$⊢ \{z \in A \| rank (z) = rank (x)\} = \{y \in A \| rank (y) = rank (x)\}$
16	6 15	eqtrdi	$⊢ v = x \to \{z \in A \| rank (z) = rank (v)\} = \{y \in A \| rank (y) = rank (x)\}$
17	3 16	weeq12d	$⊢ v = x \to (U We \{z \in A \| rank (z) = rank (v)\} \leftrightarrow R We \{y \in A \| rank (y) = rank (x)\})$
18	17	rspccva	$⊢ (\forall v \in A U We \{z \in A \| rank (z) = rank (v)\} \land x \in A) \to R We \{y \in A \| rank (y) = rank (x)\}$
19		rankfo	$⊢ rank : V \underset{onto}{⟶} On$
20		fof	$⊢ rank : V \underset{onto}{⟶} On \to rank : V ⟶ On$
21	19 20	ax-mp	$⊢ rank : V ⟶ On$
22		ssv	$⊢ A \subseteq V$
23		fssres	$⊢ (rank : V ⟶ On \land A \subseteq V) \to ({rank ↾}_{A}) : A ⟶ On$
24	21 22 23	mp2an	$⊢ ({rank ↾}_{A}) : A ⟶ On$
25	24	a1i	$⊢ \forall v \in A U We \{z \in A \| rank (z) = rank (v)\} \to ({rank ↾}_{A}) : A ⟶ On$
26		epweon	$⊢ E We On$
27	26	a1i	$⊢ \forall v \in A U We \{z \in A \| rank (z) = rank (v)\} \to E We On$
28	2 13 18 25 27	fnwe2	$⊢ \forall v \in A U We \{z \in A \| rank (z) = rank (v)\} \to S We A$
29	8 28	sylbir	$⊢ \forall x \in A R We \{z \in A \| rank (z) = rank (x)\} \to S We A$

Metamath Proof Explorer

Theorem werankwe

Proof