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 ⊢ 𝐴 ∈ V
Assertion wofib ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ↔ ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) )

Proof

Step Hyp Ref Expression
1 wofib.1 ⊢ 𝐴 ∈ V
2 wofi ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → 𝑅 We 𝐴 )
3 cnvso ⊢ ( 𝑅 Or 𝐴 ↔ ◡ 𝑅 Or 𝐴 )
4 wofi ⊢ ( ( ◡ 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 We 𝐴 )
5 3 4 sylanb ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ◡ 𝑅 We 𝐴 )
6 2 5 jca ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) → ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) )
7 weso ⊢ ( 𝑅 We 𝐴 → 𝑅 Or 𝐴 )
8 7 adantr ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → 𝑅 Or 𝐴 )
9 peano2 ⊢ ( 𝑦 ∈ ω → suc 𝑦 ∈ ω )
10 sucidg ⊢ ( 𝑦 ∈ ω → 𝑦 ∈ suc 𝑦 )
11 vex ⊢ 𝑧 ∈ V
12 vex ⊢ 𝑦 ∈ V
13 11 12 brcnv ⊢ ( 𝑧 ◡ E 𝑦 ↔ 𝑦 E 𝑧 )
14 epel ⊢ ( 𝑦 E 𝑧 ↔ 𝑦 ∈ 𝑧 )
15 13 14 bitri ⊢ ( 𝑧 ◡ E 𝑦 ↔ 𝑦 ∈ 𝑧 )
16 eleq2 ⊢ ( 𝑧 = suc 𝑦 → ( 𝑦 ∈ 𝑧 ↔ 𝑦 ∈ suc 𝑦 ) )
17 15 16 bitrid ⊢ ( 𝑧 = suc 𝑦 → ( 𝑧 ◡ E 𝑦 ↔ 𝑦 ∈ suc 𝑦 ) )
18 17 rspcev ⊢ ( ( suc 𝑦 ∈ ω ∧ 𝑦 ∈ suc 𝑦 ) → ∃ 𝑧 ∈ ω 𝑧 ◡ E 𝑦 )
19 9 10 18 syl2anc ⊢ ( 𝑦 ∈ ω → ∃ 𝑧 ∈ ω 𝑧 ◡ E 𝑦 )
20 dfrex2 ⊢ ( ∃ 𝑧 ∈ ω 𝑧 ◡ E 𝑦 ↔ ¬ ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 )
21 19 20 sylib ⊢ ( 𝑦 ∈ ω → ¬ ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 )
22 21 nrex ⊢ ¬ ∃ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦
23 ordom ⊢ Ord ω
24 eqid ⊢ OrdIso ( 𝑅 , 𝐴 ) = OrdIso ( 𝑅 , 𝐴 )
25 24 oicl ⊢ Ord dom OrdIso ( 𝑅 , 𝐴 )
26 ordtri1 ⊢ ( ( Ord ω ∧ Ord dom OrdIso ( 𝑅 , 𝐴 ) ) → ( ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ↔ ¬ dom OrdIso ( 𝑅 , 𝐴 ) ∈ ω ) )
27 23 25 26 mp2an ⊢ ( ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ↔ ¬ dom OrdIso ( 𝑅 , 𝐴 ) ∈ ω )
28 24 oion ⊢ ( 𝐴 ∈ V → dom OrdIso ( 𝑅 , 𝐴 ) ∈ On )
29 1 28 mp1i ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → dom OrdIso ( 𝑅 , 𝐴 ) ∈ On )
30 simpr ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) )
31 29 30 ssexd ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → ω ∈ V )
32 24 oiiso ⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ) → OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
33 1 32 mpan ⊢ ( 𝑅 We 𝐴 → OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
34 isocnv2 ⊢ ( OrdIso ( 𝑅 , 𝐴 ) Isom E , 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) ↔ OrdIso ( 𝑅 , 𝐴 ) Isom ◡ E , ◡ 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
35 33 34 sylib ⊢ ( 𝑅 We 𝐴 → OrdIso ( 𝑅 , 𝐴 ) Isom ◡ E , ◡ 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) )
36 wefr ⊢ ( ◡ 𝑅 We 𝐴 → ◡ 𝑅 Fr 𝐴 )
37 isofr ⊢ ( OrdIso ( 𝑅 , 𝐴 ) Isom ◡ E , ◡ 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) → ( ◡ E Fr dom OrdIso ( 𝑅 , 𝐴 ) ↔ ◡ 𝑅 Fr 𝐴 ) )
38 37 biimpar ⊢ ( ( OrdIso ( 𝑅 , 𝐴 ) Isom ◡ E , ◡ 𝑅 ( dom OrdIso ( 𝑅 , 𝐴 ) , 𝐴 ) ∧ ◡ 𝑅 Fr 𝐴 ) → ◡ E Fr dom OrdIso ( 𝑅 , 𝐴 ) )
39 35 36 38 syl2an ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → ◡ E Fr dom OrdIso ( 𝑅 , 𝐴 ) )
40 39 adantr ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → ◡ E Fr dom OrdIso ( 𝑅 , 𝐴 ) )
41 1onn ⊢ 1o ∈ ω
42 ne0i ⊢ ( 1o ∈ ω → ω ≠ ∅ )
43 41 42 mp1i ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → ω ≠ ∅ )
44 fri ⊢ ( ( ( ω ∈ V ∧ ◡ E Fr dom OrdIso ( 𝑅 , 𝐴 ) ) ∧ ( ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ∧ ω ≠ ∅ ) ) → ∃ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 )
45 31 40 30 43 44 syl22anc ⊢ ( ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) ∧ ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → ∃ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 )
46 45 ex ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → ( ω ⊆ dom OrdIso ( 𝑅 , 𝐴 ) → ∃ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 ) )
47 27 46 syl5bir ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → ( ¬ dom OrdIso ( 𝑅 , 𝐴 ) ∈ ω → ∃ 𝑦 ∈ ω ∀ 𝑧 ∈ ω ¬ 𝑧 ◡ E 𝑦 ) )
48 22 47 mt3i ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → dom OrdIso ( 𝑅 , 𝐴 ) ∈ ω )
49 ssid ⊢ dom OrdIso ( 𝑅 , 𝐴 ) ⊆ dom OrdIso ( 𝑅 , 𝐴 )
50 ssnnfi ⊢ ( ( dom OrdIso ( 𝑅 , 𝐴 ) ∈ ω ∧ dom OrdIso ( 𝑅 , 𝐴 ) ⊆ dom OrdIso ( 𝑅 , 𝐴 ) ) → dom OrdIso ( 𝑅 , 𝐴 ) ∈ Fin )
51 48 49 50 sylancl ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → dom OrdIso ( 𝑅 , 𝐴 ) ∈ Fin )
52 simpl ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → 𝑅 We 𝐴 )
53 24 oien ⊢ ( ( 𝐴 ∈ V ∧ 𝑅 We 𝐴 ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 )
54 1 52 53 sylancr ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 )
55 enfi ⊢ ( dom OrdIso ( 𝑅 , 𝐴 ) ≈ 𝐴 → ( dom OrdIso ( 𝑅 , 𝐴 ) ∈ Fin ↔ 𝐴 ∈ Fin ) )
56 54 55 syl ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → ( dom OrdIso ( 𝑅 , 𝐴 ) ∈ Fin ↔ 𝐴 ∈ Fin ) )
57 51 56 mpbid ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → 𝐴 ∈ Fin )
58 8 57 jca ⊢ ( ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) → ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) )
59 6 58 impbii ⊢ ( ( 𝑅 Or 𝐴 ∧ 𝐴 ∈ Fin ) ↔ ( 𝑅 We 𝐴 ∧ ◡ 𝑅 We 𝐴 ) )