Metamath Proof Explorer

Theorem onnseq

Description: There are no length _om decreasing sequences in the ordinals. See also noinfep for a stronger version assuming Regularity. (Contributed by Mario Carneiro, 19-May-2015)

Ref Expression
Assertion onnseq ( ( 𝐹 ‘ ∅ ) ∈ On → ∃ 𝑥 ∈ ω ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 epweon ⊢ E We On
2 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∅ ) )
3 2 eleq1d ⊢ ( 𝑦 = ∅ → ( ( 𝐹 ‘ 𝑦 ) ∈ On ↔ ( 𝐹 ‘ ∅ ) ∈ On ) )
4 fveq2 ⊢ ( 𝑦 = 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑧 ) )
5 4 eleq1d ⊢ ( 𝑦 = 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ On ↔ ( 𝐹 ‘ 𝑧 ) ∈ On ) )
6 fveq2 ⊢ ( 𝑦 = suc 𝑧 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ suc 𝑧 ) )
7 6 eleq1d ⊢ ( 𝑦 = suc 𝑧 → ( ( 𝐹 ‘ 𝑦 ) ∈ On ↔ ( 𝐹 ‘ suc 𝑧 ) ∈ On ) )
8 simpl ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ ∅ ) ∈ On )
9 suceq ⊢ ( 𝑥 = 𝑧 → suc 𝑥 = suc 𝑧 )
10 9 fveq2d ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑧 ) )
11 fveq2 ⊢ ( 𝑥 = 𝑧 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑧 ) )
12 10 11 eleq12d ⊢ ( 𝑥 = 𝑧 → ( ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
13 12 rspcv ⊢ ( 𝑧 ∈ ω → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ) )
14 onelon ⊢ ( ( ( 𝐹 ‘ 𝑧 ) ∈ On ∧ ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) ) → ( 𝐹 ‘ suc 𝑧 ) ∈ On )
15 14 expcom ⊢ ( ( 𝐹 ‘ suc 𝑧 ) ∈ ( 𝐹 ‘ 𝑧 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ On → ( 𝐹 ‘ suc 𝑧 ) ∈ On ) )
16 13 15 syl6 ⊢ ( 𝑧 ∈ ω → ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ On → ( 𝐹 ‘ suc 𝑧 ) ∈ On ) ) )
17 16 adantld ⊢ ( 𝑧 ∈ ω → ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( ( 𝐹 ‘ 𝑧 ) ∈ On → ( 𝐹 ‘ suc 𝑧 ) ∈ On ) ) )
18 3 5 7 8 17 finds2 ⊢ ( 𝑦 ∈ ω → ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝐹 ‘ 𝑦 ) ∈ On ) )
19 18 com12 ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ∈ ω → ( 𝐹 ‘ 𝑦 ) ∈ On ) )
20 19 ralrimiv ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ∀ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ∈ On )
21 eqid ⊢ ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) )
22 21 fmpt ⊢ ( ∀ 𝑦 ∈ ω ( 𝐹 ‘ 𝑦 ) ∈ On ↔ ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) : ω ⟶ On )
23 20 22 sylib ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) : ω ⟶ On )
24 23 frnd ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ⊆ On )
25 peano1 ⊢ ∅ ∈ ω
26 23 fdmd ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → dom ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) = ω )
27 25 26 eleqtrrid ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ∅ ∈ dom ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) )
28 27 ne0d ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → dom ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
29 dm0rn0 ⊢ ( dom ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) = ∅ ↔ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) = ∅ )
30 29 necon3bii ⊢ ( dom ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ↔ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
31 28 30 sylib ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ )
32 wefrc ⊢ ( ( E We On ∧ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ⊆ On ∧ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ≠ ∅ ) → ∃ 𝑧 ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ∅ )
33 1 24 31 32 mp3an2i ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑧 ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ∅ )
34 fvex ⊢ ( 𝐹 ‘ 𝑤 ) ∈ V
35 34 rgenw ⊢ ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ V
36 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
37 36 cbvmptv ⊢ ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) = ( 𝑤 ∈ ω ↦ ( 𝐹 ‘ 𝑤 ) )
38 ineq2 ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) )
39 38 eqeq1d ⊢ ( 𝑧 = ( 𝐹 ‘ 𝑤 ) → ( ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ∅ ↔ ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
40 37 39 rexrnmptw ⊢ ( ∀ 𝑤 ∈ ω ( 𝐹 ‘ 𝑤 ) ∈ V → ( ∃ 𝑧 ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ∅ ↔ ∃ 𝑤 ∈ ω ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ ) )
41 35 40 ax-mp ⊢ ( ∃ 𝑧 ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ 𝑧 ) = ∅ ↔ ∃ 𝑤 ∈ ω ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ )
42 33 41 sylib ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ∃ 𝑤 ∈ ω ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ )
43 peano2 ⊢ ( 𝑤 ∈ ω → suc 𝑤 ∈ ω )
44 43 adantl ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → suc 𝑤 ∈ ω )
45 eqid ⊢ ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ suc 𝑤 )
46 fveq2 ⊢ ( 𝑦 = suc 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ suc 𝑤 ) )
47 46 rspceeqv ⊢ ( ( suc 𝑤 ∈ ω ∧ ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ suc 𝑤 ) ) → ∃ 𝑦 ∈ ω ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
48 44 45 47 sylancl ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ∃ 𝑦 ∈ ω ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
49 fvex ⊢ ( 𝐹 ‘ suc 𝑤 ) ∈ V
50 21 elrnmpt ⊢ ( ( 𝐹 ‘ suc 𝑤 ) ∈ V → ( ( 𝐹 ‘ suc 𝑤 ) ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ ω ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ 𝑦 ) ) )
51 49 50 ax-mp ⊢ ( ( 𝐹 ‘ suc 𝑤 ) ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ↔ ∃ 𝑦 ∈ ω ( 𝐹 ‘ suc 𝑤 ) = ( 𝐹 ‘ 𝑦 ) )
52 48 51 sylibr ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ suc 𝑤 ) ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) )
53 suceq ⊢ ( 𝑥 = 𝑤 → suc 𝑥 = suc 𝑤 )
54 53 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑤 ) )
55 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
56 54 55 eleq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ( 𝐹 ‘ suc 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
57 56 rspccva ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ suc 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
58 57 adantll ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ suc 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) )
59 inelcm ⊢ ( ( ( 𝐹 ‘ suc 𝑤 ) ∈ ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∧ ( 𝐹 ‘ suc 𝑤 ) ∈ ( 𝐹 ‘ 𝑤 ) ) → ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) ≠ ∅ )
60 52 58 59 syl2anc ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) ≠ ∅ )
61 60 neneqd ⊢ ( ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ¬ ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ )
62 61 nrexdv ⊢ ( ( ( 𝐹 ‘ ∅ ) ∈ On ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ) → ¬ ∃ 𝑤 ∈ ω ( ran ( 𝑦 ∈ ω ↦ ( 𝐹 ‘ 𝑦 ) ) ∩ ( 𝐹 ‘ 𝑤 ) ) = ∅ )
63 42 62 pm2.65da ⊢ ( ( 𝐹 ‘ ∅ ) ∈ On → ¬ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
64 rexnal ⊢ ( ∃ 𝑥 ∈ ω ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) ↔ ¬ ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )
65 63 64 sylibr ⊢ ( ( 𝐹 ‘ ∅ ) ∈ On → ∃ 𝑥 ∈ ω ¬ ( 𝐹 ‘ suc 𝑥 ) ∈ ( 𝐹 ‘ 𝑥 ) )