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 𝐴 → < We 𝐴 ) )

Proof

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