Metamath Proof Explorer

Theorem finorwe

Description: If the Axiom of Infinity is denied, every total order is a well-order. The notion of a well-order cannot be usefully expressed without the Axiom of Infinity due to the inability to quantify over proper classes. (Contributed by ML, 5-Oct-2023)

Ref Expression
Assertion finorwe ⊢ ¬ ω ∈ V → < ˙ Or A → < ˙ We A

Proof

Step Hyp Ref Expression
1 simpl ⊢ ¬ ω ∈ V ∧ < ˙ Or A → ¬ ω ∈ V
2 soss ⊢ x ⊆ A → < ˙ Or A → < ˙ Or x
3 2 com12 ⊢ < ˙ Or A → x ⊆ A → < ˙ Or x
4 3 adantl ⊢ ¬ ω ∈ V ∧ < ˙ Or A → x ⊆ A → < ˙ Or x
5 vex ⊢ x ∈ V
6 fineqv ⊢ ¬ ω ∈ V ↔ Fin = V
7 6 biimpi ⊢ ¬ ω ∈ V → Fin = V
8 5 7 eleqtrrid ⊢ ¬ ω ∈ V → x ∈ Fin
9 wofi ⊢ < ˙ Or x ∧ x ∈ Fin → < ˙ We x
10 9 ancoms ⊢ x ∈ Fin ∧ < ˙ Or x → < ˙ We x
11 8 10 sylan ⊢ ¬ ω ∈ V ∧ < ˙ Or x → < ˙ We x
12 1 4 11 syl6an ⊢ ¬ ω ∈ V ∧ < ˙ Or A → x ⊆ A → < ˙ We x
13 ssid ⊢ x ⊆ x
14 wereu ⊢ < ˙ We x ∧ x ∈ V ∧ x ⊆ x ∧ x ≠ ∅ → ∃! y ∈ x ∀ z ∈ x ¬ z < ˙ y
15 reurex ⊢ ∃! y ∈ x ∀ z ∈ x ¬ z < ˙ y → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
16 14 15 syl ⊢ < ˙ We x ∧ x ∈ V ∧ x ⊆ x ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
17 5 16 mp3anr1 ⊢ < ˙ We x ∧ x ⊆ x ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
18 13 17 mpanr1 ⊢ < ˙ We x ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
19 18 ex ⊢ < ˙ We x → x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
20 12 19 syl6 ⊢ ¬ ω ∈ V ∧ < ˙ Or A → x ⊆ A → x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
21 20 impd ⊢ ¬ ω ∈ V ∧ < ˙ Or A → x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
22 21 alrimiv ⊢ ¬ ω ∈ V ∧ < ˙ Or A → ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
23 df-fr ⊢ < ˙ Fr A ↔ ∀ x x ⊆ A ∧ x ≠ ∅ → ∃ y ∈ x ∀ z ∈ x ¬ z < ˙ y
24 22 23 sylibr ⊢ ¬ ω ∈ V ∧ < ˙ Or A → < ˙ Fr A
25 simpr ⊢ ¬ ω ∈ V ∧ < ˙ Or A → < ˙ Or A
26 df-we ⊢ < ˙ We A ↔ < ˙ Fr A ∧ < ˙ Or A
27 24 25 26 sylanbrc ⊢ ¬ ω ∈ V ∧ < ˙ Or A → < ˙ We A
28 27 ex ⊢ ¬ ω ∈ V → < ˙ Or A → < ˙ We A