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 𝑥 ) ∈ ( 𝐹𝑥 ) )