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 ∈ rank ⁡ y ∨ rank ⁡ x = rank ⁡ y ∧ x R y
Assertion werankwe2 ⊢ ∀ w ∈ A R We z ∈ A | rank ⁡ z = rank ⁡ w → S We A

Proof

Step Hyp Ref Expression
1 werankwe2.1 ⊢ S = x y | rank ⁡ x ∈ rank ⁡ y ∨ rank ⁡ x = rank ⁡ y ∧ x R y
2 eqidd ⊢ v = rank ⁡ x → R = R
3 fvex ⊢ rank ⁡ y ∈ V
4 3 epeli ⊢ rank ⁡ x E rank ⁡ y ↔ rank ⁡ x ∈ rank ⁡ y
5 4 orbi1i ⊢ rank ⁡ x E rank ⁡ y ∨ rank ⁡ x = rank ⁡ y ∧ x R y ↔ rank ⁡ x ∈ 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 ∈ 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 ∈ A | rank ⁡ z = rank ⁡ w = z ∈ A | rank ⁡ z = rank ⁡ x
12 fveqeq2 ⊢ z = y → rank ⁡ z = rank ⁡ x ↔ rank ⁡ y = rank ⁡ x
13 12 cbvrabv ⊢ z ∈ A | rank ⁡ z = rank ⁡ x = y ∈ A | rank ⁡ y = rank ⁡ x
14 11 13 eqtrdi ⊢ w = x → z ∈ A | rank ⁡ z = rank ⁡ w = y ∈ A | rank ⁡ y = rank ⁡ x
15 8 14 weeq12d ⊢ w = x → R We z ∈ A | rank ⁡ z = rank ⁡ w ↔ R We y ∈ A | rank ⁡ y = rank ⁡ x
16 15 rspccva ⊢ ∀ w ∈ A R We z ∈ A | rank ⁡ z = rank ⁡ w ∧ x ∈ A → R We y ∈ 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 ⊆ V
21 fssres ⊢ rank : V ⟶ On ∧ A ⊆ V → rank ↾ A : A ⟶ On
22 19 20 21 mp2an ⊢ rank ↾ A : A ⟶ On
23 22 a1i ⊢ ∀ w ∈ A R We z ∈ A | rank ⁡ z = rank ⁡ w → rank ↾ A : A ⟶ On
24 epweon ⊢ E We On
25 24 a1i ⊢ ∀ w ∈ A R We z ∈ A | rank ⁡ z = rank ⁡ w → E We On
26 2 7 16 23 25 fnwe2 ⊢ ∀ w ∈ A R We z ∈ A | rank ⁡ z = rank ⁡ w → S We A