Metamath Proof Explorer

Theorem vonf1owev

Description: If F is a bijection from the universe to the ordinals, then R well-orders the universe. This is the ZFC version of (2 -> 3) in https://tinyurl.com/hamkins-gblac . (Contributed by BTernaryTau, 6-Dec-2025)

Ref Expression
Hypothesis vonf1owev.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
Assertion vonf1owev ( 𝐹 : V –1-1-onto→ On → 𝑅 We V )

Proof

Step Hyp Ref Expression
1 vonf1owev.1 ⊢ 𝑅 = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) }
2 f1of ⊢ ( 𝐹 : V –1-1-onto→ On → 𝐹 : V ⟶ On )
3 2 fimassd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 “ 𝑡 ) ⊆ On )
4 f1odm ⊢ ( 𝐹 : V –1-1-onto→ On → dom 𝐹 = V )
5 4 ineq1d ⊢ ( 𝐹 : V –1-1-onto→ On → ( dom 𝐹 ∩ 𝑡 ) = ( V ∩ 𝑡 ) )
6 5 neeq1d ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( dom 𝐹 ∩ 𝑡 ) ≠ ∅ ↔ ( V ∩ 𝑡 ) ≠ ∅ ) )
7 inv1 ⊢ ( 𝑡 ∩ V ) = 𝑡
8 7 ineqcomi ⊢ ( V ∩ 𝑡 ) = 𝑡
9 8 neeq1i ⊢ ( ( V ∩ 𝑡 ) ≠ ∅ ↔ 𝑡 ≠ ∅ )
10 6 9 bitr2di ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝑡 ≠ ∅ ↔ ( dom 𝐹 ∩ 𝑡 ) ≠ ∅ ) )
11 10 biimpa ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑡 ≠ ∅ ) → ( dom 𝐹 ∩ 𝑡 ) ≠ ∅ )
12 11 imadisjlnd ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑡 ≠ ∅ ) → ( 𝐹 “ 𝑡 ) ≠ ∅ )
13 onssmin ⊢ ( ( ( 𝐹 “ 𝑡 ) ⊆ On ∧ ( 𝐹 “ 𝑡 ) ≠ ∅ ) → ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 )
14 3 12 13 syl2an2r ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑡 ≠ ∅ ) → ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 )
15 14 ex ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝑡 ≠ ∅ → ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 ) )
16 vex ⊢ 𝑣 ∈ V
17 vex ⊢ 𝑢 ∈ V
18 fveq2 ⊢ ( 𝑥 = 𝑣 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑣 ) )
19 18 eleq1d ⊢ ( 𝑥 = 𝑣 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
20 fveq2 ⊢ ( 𝑦 = 𝑢 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑢 ) )
21 20 eleq2d ⊢ ( 𝑦 = 𝑢 → ( ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑢 ) ) )
22 16 17 19 21 1 brab ⊢ ( 𝑣 𝑅 𝑢 ↔ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑢 ) )
23 22 notbii ⊢ ( ¬ 𝑣 𝑅 𝑢 ↔ ¬ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑢 ) )
24 2 ffvelcdmda ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑢 ∈ V ) → ( 𝐹 ‘ 𝑢 ) ∈ On )
25 24 elvd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 ‘ 𝑢 ) ∈ On )
26 2 ffvelcdmda ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑣 ∈ V ) → ( 𝐹 ‘ 𝑣 ) ∈ On )
27 26 elvd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 ‘ 𝑣 ) ∈ On )
28 ontri1 ⊢ ( ( ( 𝐹 ‘ 𝑢 ) ∈ On ∧ ( 𝐹 ‘ 𝑣 ) ∈ On ) → ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ↔ ¬ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑢 ) ) )
29 25 27 28 syl2anc ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ↔ ¬ ( 𝐹 ‘ 𝑣 ) ∈ ( 𝐹 ‘ 𝑢 ) ) )
30 23 29 bitr4id ⊢ ( 𝐹 : V –1-1-onto→ On → ( ¬ 𝑣 𝑅 𝑢 ↔ ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) )
31 30 ralbidv ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ↔ ∀ 𝑣 ∈ 𝑡 ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) )
32 f1ofn ⊢ ( 𝐹 : V –1-1-onto→ On → 𝐹 Fn V )
33 ssv ⊢ 𝑡 ⊆ V
34 sseq2 ⊢ ( 𝑠 = ( 𝐹 ‘ 𝑣 ) → ( ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ↔ ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) )
35 34 ralima ⊢ ( ( 𝐹 Fn V ∧ 𝑡 ⊆ V ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ↔ ∀ 𝑣 ∈ 𝑡 ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) )
36 32 33 35 sylancl ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ↔ ∀ 𝑣 ∈ 𝑡 ( 𝐹 ‘ 𝑢 ) ⊆ ( 𝐹 ‘ 𝑣 ) ) )
37 31 36 bitr4d ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ↔ ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
38 37 rexbidv ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ↔ ∃ 𝑢 ∈ 𝑡 ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
39 sseq1 ⊢ ( 𝑟 = ( 𝐹 ‘ 𝑢 ) → ( 𝑟 ⊆ 𝑠 ↔ ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
40 39 ralbidv ⊢ ( 𝑟 = ( 𝐹 ‘ 𝑢 ) → ( ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 ↔ ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
41 40 rexima ⊢ ( ( 𝐹 Fn V ∧ 𝑡 ⊆ V ) → ( ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 ↔ ∃ 𝑢 ∈ 𝑡 ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
42 32 33 41 sylancl ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 ↔ ∃ 𝑢 ∈ 𝑡 ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) ( 𝐹 ‘ 𝑢 ) ⊆ 𝑠 ) )
43 38 42 bitr4d ⊢ ( 𝐹 : V –1-1-onto→ On → ( ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ↔ ∃ 𝑟 ∈ ( 𝐹 “ 𝑡 ) ∀ 𝑠 ∈ ( 𝐹 “ 𝑡 ) 𝑟 ⊆ 𝑠 ) )
44 15 43 sylibrd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝑡 ≠ ∅ → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
45 44 alrimiv ⊢ ( 𝐹 : V –1-1-onto→ On → ∀ 𝑡 ( 𝑡 ≠ ∅ → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
46 df-fr ⊢ ( 𝑅 Fr V ↔ ∀ 𝑡 ( ( 𝑡 ⊆ V ∧ 𝑡 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
47 33 biantrur ⊢ ( 𝑡 ≠ ∅ ↔ ( 𝑡 ⊆ V ∧ 𝑡 ≠ ∅ ) )
48 47 imbi1i ⊢ ( ( 𝑡 ≠ ∅ → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) ↔ ( ( 𝑡 ⊆ V ∧ 𝑡 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
49 48 albii ⊢ ( ∀ 𝑡 ( 𝑡 ≠ ∅ → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) ↔ ∀ 𝑡 ( ( 𝑡 ⊆ V ∧ 𝑡 ≠ ∅ ) → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
50 46 49 bitr4i ⊢ ( 𝑅 Fr V ↔ ∀ 𝑡 ( 𝑡 ≠ ∅ → ∃ 𝑢 ∈ 𝑡 ∀ 𝑣 ∈ 𝑡 ¬ 𝑣 𝑅 𝑢 ) )
51 45 50 sylibr ⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 Fr V )
52 2 ffvelcdmda ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑤 ∈ V ) → ( 𝐹 ‘ 𝑤 ) ∈ On )
53 52 elvd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 ‘ 𝑤 ) ∈ On )
54 2 ffvelcdmda ⊢ ( ( 𝐹 : V –1-1-onto→ On ∧ 𝑧 ∈ V ) → ( 𝐹 ‘ 𝑧 ) ∈ On )
55 54 elvd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝐹 ‘ 𝑧 ) ∈ On )
56 oneltri ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ On ∧ ( 𝐹 ‘ 𝑧 ) ∈ On ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) )
57 53 55 56 syl2anc ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) )
58 3orcomb ⊢ ( ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ) ↔ ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
59 57 58 sylib ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
60 vex ⊢ 𝑤 ∈ V
61 vex ⊢ 𝑧 ∈ V
62 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
63 62 eleq1d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
64 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
65 64 eleq2d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
66 60 61 63 65 1 brab ⊢ ( 𝑤 𝑅 𝑧 ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) )
67 66 biimpri ⊢ ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) → 𝑤 𝑅 𝑧 )
68 67 a1i ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) → 𝑤 𝑅 𝑧 ) )
69 f1of1 ⊢ ( 𝐹 : V –1-1-onto→ On → 𝐹 : V –1-1→ On )
70 f1veqaeq ⊢ ( ( 𝐹 : V –1-1→ On ∧ ( 𝑤 ∈ V ∧ 𝑧 ∈ V ) ) → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
71 60 61 70 mpanr12 ⊢ ( 𝐹 : V –1-1→ On → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
72 69 71 syl ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) → 𝑤 = 𝑧 ) )
73 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
74 73 eleq1d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) )
75 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
76 75 eleq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
77 61 60 74 76 1 brab ⊢ ( 𝑧 𝑅 𝑤 ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) )
78 77 biimpri ⊢ ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → 𝑧 𝑅 𝑤 )
79 78 a1i ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → 𝑧 𝑅 𝑤 ) )
80 68 72 79 3orim123d ⊢ ( 𝐹 : V –1-1-onto→ On → ( ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑤 ) = ( 𝐹 ‘ 𝑧 ) ∨ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) → ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) ) )
81 59 80 mpd ⊢ ( 𝐹 : V –1-1-onto→ On → ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
82 81 ralrimivw ⊢ ( 𝐹 : V –1-1-onto→ On → ∀ 𝑧 ∈ V ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
83 82 ralrimivw ⊢ ( 𝐹 : V –1-1-onto→ On → ∀ 𝑤 ∈ V ∀ 𝑧 ∈ V ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) )
84 dfwe2 ⊢ ( 𝑅 We V ↔ ( 𝑅 Fr V ∧ ∀ 𝑤 ∈ V ∀ 𝑧 ∈ V ( 𝑤 𝑅 𝑧 ∨ 𝑤 = 𝑧 ∨ 𝑧 𝑅 𝑤 ) ) )
85 51 83 84 sylanbrc ⊢ ( 𝐹 : V –1-1-onto→ On → 𝑅 We V )