Metamath Proof Explorer

Theorem wofib

Description: The only sets which are well-ordered forwards and backwards are finite sets. (Contributed by Mario Carneiro, 30-Jan-2014) (Revised by Mario Carneiro, 23-May-2015)

Ref Expression
Hypothesis wofib.1 
|- A e. _V
Assertion wofib 
|- ( ( R Or A /\ A e. Fin ) <-> ( R We A /\ `' R We A ) )

Proof

Step Hyp Ref Expression
1 wofib.1 
 |-  A e. _V
2 wofi 
 |-  ( ( R Or A /\ A e. Fin ) -> R We A )
3 cnvso 
 |-  ( R Or A <-> `' R Or A )
4 wofi 
 |-  ( ( `' R Or A /\ A e. Fin ) -> `' R We A )
5 3 4 sylanb 
 |-  ( ( R Or A /\ A e. Fin ) -> `' R We A )
6 2 5 jca 
 |-  ( ( R Or A /\ A e. Fin ) -> ( R We A /\ `' R We A ) )
7 weso 
 |-  ( R We A -> R Or A )
8 7 adantr 
 |-  ( ( R We A /\ `' R We A ) -> R Or A )
9 peano2 
 |-  ( y e. _om -> suc y e. _om )
10 sucidg 
 |-  ( y e. _om -> y e. suc y )
11 vex 
 |-  z e. _V
12 vex 
 |-  y e. _V
13 11 12 brcnv 
 |-  ( z `' _E y <-> y _E z )
14 epel 
 |-  ( y _E z <-> y e. z )
15 13 14 bitri 
 |-  ( z `' _E y <-> y e. z )
16 eleq2 
 |-  ( z = suc y -> ( y e. z <-> y e. suc y ) )
17 15 16 syl5bb 
 |-  ( z = suc y -> ( z `' _E y <-> y e. suc y ) )
18 17 rspcev 
 |-  ( ( suc y e. _om /\ y e. suc y ) -> E. z e. _om z `' _E y )
19 9 10 18 syl2anc 
 |-  ( y e. _om -> E. z e. _om z `' _E y )
20 dfrex2 
 |-  ( E. z e. _om z `' _E y <-> -. A. z e. _om -. z `' _E y )
21 19 20 sylib 
 |-  ( y e. _om -> -. A. z e. _om -. z `' _E y )
22 21 nrex 
 |-  -. E. y e. _om A. z e. _om -. z `' _E y
23 ordom 
 |-  Ord _om
24 eqid 
 |-  OrdIso ( R , A ) = OrdIso ( R , A )
25 24 oicl 
 |-  Ord dom OrdIso ( R , A )
26 ordtri1 
 |-  ( ( Ord _om /\ Ord dom OrdIso ( R , A ) ) -> ( _om C_ dom OrdIso ( R , A ) <-> -. dom OrdIso ( R , A ) e. _om ) )
27 23 25 26 mp2an 
 |-  ( _om C_ dom OrdIso ( R , A ) <-> -. dom OrdIso ( R , A ) e. _om )
28 24 oion 
 |-  ( A e. _V -> dom OrdIso ( R , A ) e. On )
29 1 28 mp1i 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> dom OrdIso ( R , A ) e. On )
30 simpr 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> _om C_ dom OrdIso ( R , A ) )
31 29 30 ssexd 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> _om e. _V )
32 24 oiiso 
 |-  ( ( A e. _V /\ R We A ) -> OrdIso ( R , A ) Isom _E , R ( dom OrdIso ( R , A ) , A ) )
33 1 32 mpan 
 |-  ( R We A -> OrdIso ( R , A ) Isom _E , R ( dom OrdIso ( R , A ) , A ) )
34 isocnv2 
 |-  ( OrdIso ( R , A ) Isom _E , R ( dom OrdIso ( R , A ) , A ) <-> OrdIso ( R , A ) Isom `' _E , `' R ( dom OrdIso ( R , A ) , A ) )
35 33 34 sylib 
 |-  ( R We A -> OrdIso ( R , A ) Isom `' _E , `' R ( dom OrdIso ( R , A ) , A ) )
36 wefr 
 |-  ( `' R We A -> `' R Fr A )
37 isofr 
 |-  ( OrdIso ( R , A ) Isom `' _E , `' R ( dom OrdIso ( R , A ) , A ) -> ( `' _E Fr dom OrdIso ( R , A ) <-> `' R Fr A ) )
38 37 biimpar 
 |-  ( ( OrdIso ( R , A ) Isom `' _E , `' R ( dom OrdIso ( R , A ) , A ) /\ `' R Fr A ) -> `' _E Fr dom OrdIso ( R , A ) )
39 35 36 38 syl2an 
 |-  ( ( R We A /\ `' R We A ) -> `' _E Fr dom OrdIso ( R , A ) )
40 39 adantr 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> `' _E Fr dom OrdIso ( R , A ) )
41 1onn 
 |-  1o e. _om
42 ne0i 
 |-  ( 1o e. _om -> _om =/= (/) )
43 41 42 mp1i 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> _om =/= (/) )
44 fri 
 |-  ( ( ( _om e. _V /\ `' _E Fr dom OrdIso ( R , A ) ) /\ ( _om C_ dom OrdIso ( R , A ) /\ _om =/= (/) ) ) -> E. y e. _om A. z e. _om -. z `' _E y )
45 31 40 30 43 44 syl22anc 
 |-  ( ( ( R We A /\ `' R We A ) /\ _om C_ dom OrdIso ( R , A ) ) -> E. y e. _om A. z e. _om -. z `' _E y )
46 45 ex 
 |-  ( ( R We A /\ `' R We A ) -> ( _om C_ dom OrdIso ( R , A ) -> E. y e. _om A. z e. _om -. z `' _E y ) )
47 27 46 syl5bir 
 |-  ( ( R We A /\ `' R We A ) -> ( -. dom OrdIso ( R , A ) e. _om -> E. y e. _om A. z e. _om -. z `' _E y ) )
48 22 47 mt3i 
 |-  ( ( R We A /\ `' R We A ) -> dom OrdIso ( R , A ) e. _om )
49 ssid 
 |-  dom OrdIso ( R , A ) C_ dom OrdIso ( R , A )
50 ssnnfi 
 |-  ( ( dom OrdIso ( R , A ) e. _om /\ dom OrdIso ( R , A ) C_ dom OrdIso ( R , A ) ) -> dom OrdIso ( R , A ) e. Fin )
51 48 49 50 sylancl 
 |-  ( ( R We A /\ `' R We A ) -> dom OrdIso ( R , A ) e. Fin )
52 simpl 
 |-  ( ( R We A /\ `' R We A ) -> R We A )
53 24 oien 
 |-  ( ( A e. _V /\ R We A ) -> dom OrdIso ( R , A ) ~~ A )
54 1 52 53 sylancr 
 |-  ( ( R We A /\ `' R We A ) -> dom OrdIso ( R , A ) ~~ A )
55 enfi 
 |-  ( dom OrdIso ( R , A ) ~~ A -> ( dom OrdIso ( R , A ) e. Fin <-> A e. Fin ) )
56 54 55 syl 
 |-  ( ( R We A /\ `' R We A ) -> ( dom OrdIso ( R , A ) e. Fin <-> A e. Fin ) )
57 51 56 mpbid 
 |-  ( ( R We A /\ `' R We A ) -> A e. Fin )
58 8 57 jca 
 |-  ( ( R We A /\ `' R We A ) -> ( R Or A /\ A e. Fin ) )
59 6 58 impbii 
 |-  ( ( R Or A /\ A e. Fin ) <-> ( R We A /\ `' R We A ) )