Metamath Proof Explorer

Theorem vonf1osev

Description: If F is a bijection from the universe to the ordinals, then R is a set-like well-ordering of the universe. This is the ZFC version of (2 -> 4) which is used in place of (3 -> 4) in https://tinyurl.com/hamkins-gblac . This proof takes advantage of the fact that the well-order constructed in (2 -> 3) is also set-like. (Contributed by BTernaryTau, 8-Jun-2026)

Ref Expression
Hypothesis vonf1osev.1 ⊢ R = x y | F ⁡ x ∈ F ⁡ y
Assertion vonf1osev ⊢ F : V ⟶ 1-1 onto On → R We V ∧ R Se V

Proof

Step Hyp Ref Expression
1 vonf1osev.1 ⊢ R = x y | F ⁡ x ∈ F ⁡ y
2 1 vonf1owev ⊢ F : V ⟶ 1-1 onto On → R We V
3 vex ⊢ w ∈ V
4 vex ⊢ z ∈ V
5 fveq2 ⊢ x = w → F ⁡ x = F ⁡ w
6 5 eleq1d ⊢ x = w → F ⁡ x ∈ F ⁡ y ↔ F ⁡ w ∈ F ⁡ y
7 fveq2 ⊢ y = z → F ⁡ y = F ⁡ z
8 7 eleq2d ⊢ y = z → F ⁡ w ∈ F ⁡ y ↔ F ⁡ w ∈ F ⁡ z
9 3 4 6 8 1 brab ⊢ w R z ↔ F ⁡ w ∈ F ⁡ z
10 fvex ⊢ F ⁡ z ∈ V
11 10 epeli ⊢ F ⁡ w E F ⁡ z ↔ F ⁡ w ∈ F ⁡ z
12 9 11 bitr4i ⊢ w R z ↔ F ⁡ w E F ⁡ z
13 12 rgen2w ⊢ ∀ w ∈ V ∀ z ∈ V w R z ↔ F ⁡ w E F ⁡ z
14 df-isom ⊢ F Isom R , E V On ↔ F : V ⟶ 1-1 onto On ∧ ∀ w ∈ V ∀ z ∈ V w R z ↔ F ⁡ w E F ⁡ z
15 13 14 mpbiran2 ⊢ F Isom R , E V On ↔ F : V ⟶ 1-1 onto On
16 epse ⊢ E Se On
17 isose ⊢ F Isom R , E V On → R Se V ↔ E Se On
18 16 17 mpbiri ⊢ F Isom R , E V On → R Se V
19 15 18 sylbir ⊢ F : V ⟶ 1-1 onto On → R Se V
20 2 19 jca ⊢ F : V ⟶ 1-1 onto On → R We V ∧ R Se V