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 
|- ( -. _om e. _V -> ( .< Or A -> .< We A ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> -. _om e. _V )
2 soss 
 |-  ( x C_ A -> ( .< Or A -> .< Or x ) )
3 2 com12 
 |-  ( .< Or A -> ( x C_ A -> .< Or x ) )
4 3 adantl 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> ( x C_ A -> .< Or x ) )
5 vex 
 |-  x e. _V
6 fineqv 
 |-  ( -. _om e. _V <-> Fin = _V )
7 6 biimpi 
 |-  ( -. _om e. _V -> Fin = _V )
8 5 7 eleqtrrid 
 |-  ( -. _om e. _V -> x e. Fin )
9 wofi 
 |-  ( ( .< Or x /\ x e. Fin ) -> .< We x )
10 9 ancoms 
 |-  ( ( x e. Fin /\ .< Or x ) -> .< We x )
11 8 10 sylan 
 |-  ( ( -. _om e. _V /\ .< Or x ) -> .< We x )
12 1 4 11 syl6an 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> ( x C_ A -> .< We x ) )
13 ssid 
 |-  x C_ x
14 wereu 
 |-  ( ( .< We x /\ ( x e. _V /\ x C_ x /\ x =/= (/) ) ) -> E! y e. x A. z e. x -. z .< y )
15 reurex 
 |-  ( E! y e. x A. z e. x -. z .< y -> E. y e. x A. z e. x -. z .< y )
16 14 15 syl 
 |-  ( ( .< We x /\ ( x e. _V /\ x C_ x /\ x =/= (/) ) ) -> E. y e. x A. z e. x -. z .< y )
17 5 16 mp3anr1 
 |-  ( ( .< We x /\ ( x C_ x /\ x =/= (/) ) ) -> E. y e. x A. z e. x -. z .< y )
18 13 17 mpanr1 
 |-  ( ( .< We x /\ x =/= (/) ) -> E. y e. x A. z e. x -. z .< y )
19 18 ex 
 |-  ( .< We x -> ( x =/= (/) -> E. y e. x A. z e. x -. z .< y ) )
20 12 19 syl6 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> ( x C_ A -> ( x =/= (/) -> E. y e. x A. z e. x -. z .< y ) ) )
21 20 impd 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z .< y ) )
22 21 alrimiv 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z .< y ) )
23 df-fr 
 |-  ( .< Fr A <-> A. x ( ( x C_ A /\ x =/= (/) ) -> E. y e. x A. z e. x -. z .< y ) )
24 22 23 sylibr 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> .< Fr A )
25 simpr 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> .< Or A )
26 df-we 
 |-  ( .< We A <-> ( .< Fr A /\ .< Or A ) )
27 24 25 26 sylanbrc 
 |-  ( ( -. _om e. _V /\ .< Or A ) -> .< We A )
28 27 ex 
 |-  ( -. _om e. _V -> ( .< Or A -> .< We A ) )