Metamath Proof Explorer

Theorem omsmolem

Description: Lemma for omsmo . (Contributed by NM, 30-Nov-2003) (Revised by David Abernethy, 1-Jan-2014)

Ref Expression
Assertion omsmolem ( 𝑦 ∈ ω → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 ⊢ ( 𝑦 = ∅ → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ ∅ ) )
2 fveq2 ⊢ ( 𝑦 = ∅ → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ ∅ ) )
3 2 eleq2d ⊢ ( 𝑦 = ∅ → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ ∅ ) ) )
4 1 3 imbi12d ⊢ ( 𝑦 = ∅ → ( ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ∈ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ ∅ ) ) ) )
5 eleq2 ⊢ ( 𝑦 = 𝑤 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ 𝑤 ) )
6 fveq2 ⊢ ( 𝑦 = 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ 𝑤 ) )
7 6 eleq2d ⊢ ( 𝑦 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) )
8 5 7 imbi12d ⊢ ( 𝑦 = 𝑤 → ( ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) )
9 eleq2 ⊢ ( 𝑦 = suc 𝑤 → ( 𝑧 ∈ 𝑦 ↔ 𝑧 ∈ suc 𝑤 ) )
10 fveq2 ⊢ ( 𝑦 = suc 𝑤 → ( 𝐹 ‘ 𝑦 ) = ( 𝐹 ‘ suc 𝑤 ) )
11 10 eleq2d ⊢ ( 𝑦 = suc 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ↔ ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
12 9 11 imbi12d ⊢ ( 𝑦 = suc 𝑤 → ( ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ↔ ( 𝑧 ∈ suc 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) )
13 noel ⊢ ¬ 𝑧 ∈ ∅
14 13 pm2.21i ⊢ ( 𝑧 ∈ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ ∅ ) )
15 14 a1i ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑧 ∈ ∅ → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ ∅ ) ) )
16 vex ⊢ 𝑧 ∈ V
17 16 elsuc ⊢ ( 𝑧 ∈ suc 𝑤 ↔ ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ) )
18 fveq2 ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑤 ) )
19 suceq ⊢ ( 𝑥 = 𝑤 → suc 𝑥 = suc 𝑤 )
20 19 fveq2d ⊢ ( 𝑥 = 𝑤 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑤 ) )
21 18 20 eleq12d ⊢ ( 𝑥 = 𝑤 → ( ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
22 21 rspccva ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) )
23 22 adantll ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) )
24 peano2b ⊢ ( 𝑤 ∈ ω ↔ suc 𝑤 ∈ ω )
25 ffvelrn ⊢ ( ( 𝐹 : ω ⟶ 𝐴 ∧ suc 𝑤 ∈ ω ) → ( 𝐹 ‘ suc 𝑤 ) ∈ 𝐴 )
26 24 25 sylan2b ⊢ ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑤 ∈ ω ) → ( 𝐹 ‘ suc 𝑤 ) ∈ 𝐴 )
27 ssel ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 ‘ suc 𝑤 ) ∈ 𝐴 → ( 𝐹 ‘ suc 𝑤 ) ∈ On ) )
28 ontr1 ⊢ ( ( 𝐹 ‘ suc 𝑤 ) ∈ On → ( ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ∧ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
29 28 expcomd ⊢ ( ( 𝐹 ‘ suc 𝑤 ) ∈ On → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) )
30 26 27 29 syl56 ⊢ ( 𝐴 ⊆ On → ( ( 𝐹 : ω ⟶ 𝐴 ∧ 𝑤 ∈ ω ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) ) )
31 30 impl ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ 𝑤 ∈ ω ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) )
32 31 adantlr ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) )
33 23 32 mpd ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
34 33 imim2d ⊢ ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) → ( ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) )
35 34 imp ⊢ ( ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) ∧ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
36 fveq2 ⊢ ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) = ( 𝐹 ‘ 𝑤 ) )
37 36 eleq1d ⊢ ( 𝑧 = 𝑤 → ( ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ↔ ( 𝐹 ‘ 𝑤 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
38 22 37 syl5ibrcom ⊢ ( ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ∧ 𝑤 ∈ ω ) → ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
39 38 ad4ant23 ⊢ ( ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) ∧ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝑧 = 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
40 35 39 jaod ⊢ ( ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) ∧ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) → ( ( 𝑧 ∈ 𝑤 ∨ 𝑧 = 𝑤 ) → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
41 17 40 syl5bi ⊢ ( ( ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) ∧ 𝑤 ∈ ω ) ∧ ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) ) → ( 𝑧 ∈ suc 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) )
42 41 exp31 ⊢ ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑤 ∈ ω → ( ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 ∈ suc 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) ) )
43 42 com12 ⊢ ( 𝑤 ∈ ω → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( ( 𝑧 ∈ 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑤 ) ) → ( 𝑧 ∈ suc 𝑤 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ suc 𝑤 ) ) ) ) )
44 4 8 12 15 43 finds2 ⊢ ( 𝑦 ∈ ω → ( ( ( 𝐴 ⊆ On ∧ 𝐹 : ω ⟶ 𝐴 ) ∧ ∀ 𝑥 ∈ ω ( 𝐹 ‘ 𝑥 ) ∈ ( 𝐹 ‘ suc 𝑥 ) ) → ( 𝑧 ∈ 𝑦 → ( 𝐹 ‘ 𝑧 ) ∈ ( 𝐹 ‘ 𝑦 ) ) ) )