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 V
Assertion wofib R Or A A Fin R We A R -1 We A

Proof

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