Metamath Proof Explorer

Theorem wevsev

Description: If R is a well-ordering of the universe, then S is a set-like well-ordering of the universe. This is the ZFC version of (3 -> 4) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 18-Sep-2026)

Ref Expression
Hypothesis wevsev.1 ⊢ S = x y | rank ⁡ x ∈ rank ⁡ y ∨ rank ⁡ x = rank ⁡ y ∧ x R y
Assertion wevsev ⊢ R We V → S We V ∧ S Se V

Proof

Step Hyp Ref Expression
1 wevsev.1 ⊢ S = x y | rank ⁡ x ∈ rank ⁡ y ∨ rank ⁡ x = rank ⁡ y ∧ x R y
2 ssv ⊢ z ∈ V | rank ⁡ z = rank ⁡ w ⊆ V
3 wess ⊢ z ∈ V | rank ⁡ z = rank ⁡ w ⊆ V → R We V → R We z ∈ V | rank ⁡ z = rank ⁡ w
4 2 3 ax-mp ⊢ R We V → R We z ∈ V | rank ⁡ z = rank ⁡ w
5 4 ralrimivw ⊢ R We V → ∀ w ∈ V R We z ∈ V | rank ⁡ z = rank ⁡ w
6 1 werankwe2 ⊢ ∀ w ∈ V R We z ∈ V | rank ⁡ z = rank ⁡ w → S We V
7 5 6 syl ⊢ R We V → S We V
8 1 rankse ⊢ S Se V
9 7 8 jctir ⊢ R We V → S We V ∧ S Se V