# Metamath Proof Explorer

## Theorem isf32lem2

Description: Lemma for isfin3-2 . Non-minimum implies that there is always another decrease. (Contributed by Stefan O'Rear, 5-Nov-2014)

Ref Expression
Hypotheses isf32lem.a ( 𝜑𝐹 : ω ⟶ 𝒫 𝐺 )
isf32lem.b ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) )
isf32lem.c ( 𝜑 → ¬ ran 𝐹 ∈ ran 𝐹 )
Assertion isf32lem2 ( ( 𝜑𝐴 ∈ ω ) → ∃ 𝑎 ∈ ω ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) )

### Proof

Step Hyp Ref Expression
1 isf32lem.a ( 𝜑𝐹 : ω ⟶ 𝒫 𝐺 )
2 isf32lem.b ( 𝜑 → ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) )
3 isf32lem.c ( 𝜑 → ¬ ran 𝐹 ∈ ran 𝐹 )
4 3 adantr ( ( 𝜑𝐴 ∈ ω ) → ¬ ran 𝐹 ∈ ran 𝐹 )
5 1 ffnd ( 𝜑𝐹 Fn ω )
6 peano2 ( 𝐴 ∈ ω → suc 𝐴 ∈ ω )
7 fnfvelrn ( ( 𝐹 Fn ω ∧ suc 𝐴 ∈ ω ) → ( 𝐹 ‘ suc 𝐴 ) ∈ ran 𝐹 )
8 5 6 7 syl2an ( ( 𝜑𝐴 ∈ ω ) → ( 𝐹 ‘ suc 𝐴 ) ∈ ran 𝐹 )
9 8 adantr ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ( 𝐹 ‘ suc 𝐴 ) ∈ ran 𝐹 )
10 intss1 ( ( 𝐹 ‘ suc 𝐴 ) ∈ ran 𝐹 ran 𝐹 ⊆ ( 𝐹 ‘ suc 𝐴 ) )
11 9 10 syl ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ran 𝐹 ⊆ ( 𝐹 ‘ suc 𝐴 ) )
12 fvelrnb ( 𝐹 Fn ω → ( 𝑏 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ω ( 𝐹𝑐 ) = 𝑏 ) )
13 5 12 syl ( 𝜑 → ( 𝑏 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ω ( 𝐹𝑐 ) = 𝑏 ) )
14 13 ad2antrr ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ( 𝑏 ∈ ran 𝐹 ↔ ∃ 𝑐 ∈ ω ( 𝐹𝑐 ) = 𝑏 ) )
15 simplrr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → 𝑐 ∈ ω )
16 6 ad3antlr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → suc 𝐴 ∈ ω )
17 simpr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → suc 𝐴𝑐 )
18 simplrl ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
19 fveq2 ( 𝑏 = suc 𝐴 → ( 𝐹𝑏 ) = ( 𝐹 ‘ suc 𝐴 ) )
20 19 eqeq2d ( 𝑏 = suc 𝐴 → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ↔ ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) ) )
21 20 imbi2d ( 𝑏 = suc 𝐴 → ( ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ) ↔ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) ) ) )
22 fveq2 ( 𝑏 = 𝑑 → ( 𝐹𝑏 ) = ( 𝐹𝑑 ) )
23 22 eqeq2d ( 𝑏 = 𝑑 → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ↔ ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) ) )
24 23 imbi2d ( 𝑏 = 𝑑 → ( ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ) ↔ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) ) ) )
25 fveq2 ( 𝑏 = suc 𝑑 → ( 𝐹𝑏 ) = ( 𝐹 ‘ suc 𝑑 ) )
26 25 eqeq2d ( 𝑏 = suc 𝑑 → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ↔ ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) ) )
27 26 imbi2d ( 𝑏 = suc 𝑑 → ( ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ) ↔ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) ) ) )
28 fveq2 ( 𝑏 = 𝑐 → ( 𝐹𝑏 ) = ( 𝐹𝑐 ) )
29 28 eqeq2d ( 𝑏 = 𝑐 → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ↔ ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) ) )
30 29 imbi2d ( 𝑏 = 𝑐 → ( ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑏 ) ) ↔ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) ) ) )
31 eqid ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝐴 )
32 31 2a1i ( suc 𝐴 ∈ ω → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝐴 ) ) )
33 elex ( suc 𝐴 ∈ ω → suc 𝐴 ∈ V )
34 sucexb ( 𝐴 ∈ V ↔ suc 𝐴 ∈ V )
35 33 34 sylibr ( suc 𝐴 ∈ ω → 𝐴 ∈ V )
36 35 adantl ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) → 𝐴 ∈ V )
37 sucssel ( 𝐴 ∈ V → ( suc 𝐴𝑑𝐴𝑑 ) )
38 36 37 syl ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) → ( suc 𝐴𝑑𝐴𝑑 ) )
39 38 imp ( ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑑 ) → 𝐴𝑑 )
40 eleq2w ( 𝑎 = 𝑑 → ( 𝐴𝑎𝐴𝑑 ) )
41 suceq ( 𝑎 = 𝑑 → suc 𝑎 = suc 𝑑 )
42 41 fveq2d ( 𝑎 = 𝑑 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹 ‘ suc 𝑑 ) )
43 fveq2 ( 𝑎 = 𝑑 → ( 𝐹𝑎 ) = ( 𝐹𝑑 ) )
44 42 43 eqeq12d ( 𝑎 = 𝑑 → ( ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ↔ ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) )
45 40 44 imbi12d ( 𝑎 = 𝑑 → ( ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ↔ ( 𝐴𝑑 → ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) ) )
46 45 rspcv ( 𝑑 ∈ ω → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐴𝑑 → ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) ) )
47 46 com23 ( 𝑑 ∈ ω → ( 𝐴𝑑 → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) ) )
48 47 ad2antrr ( ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑑 ) → ( 𝐴𝑑 → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) ) )
49 39 48 mpd ( ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑑 ) → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) )
50 eqtr3 ( ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) ∧ ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) )
51 50 expcom ( ( 𝐹 ‘ suc 𝑑 ) = ( 𝐹𝑑 ) → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) ) )
52 49 51 syl6 ( ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑑 ) → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) ) ) )
53 52 a2d ( ( ( 𝑑 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑑 ) → ( ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑑 ) ) → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹 ‘ suc 𝑑 ) ) ) )
54 21 24 27 30 32 53 findsg ( ( ( 𝑐 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ suc 𝐴𝑐 ) → ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) ) )
55 54 impr ( ( ( 𝑐 ∈ ω ∧ suc 𝐴 ∈ ω ) ∧ ( suc 𝐴𝑐 ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) )
56 15 16 17 18 55 syl22anc ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) )
57 eqimss ( ( 𝐹 ‘ suc 𝐴 ) = ( 𝐹𝑐 ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
58 56 57 syl ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ suc 𝐴𝑐 ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
59 6 ad3antlr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ⊆ suc 𝐴 ) → suc 𝐴 ∈ ω )
60 simplrr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ⊆ suc 𝐴 ) → 𝑐 ∈ ω )
61 simpr ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ⊆ suc 𝐴 ) → 𝑐 ⊆ suc 𝐴 )
62 simplll ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ⊆ suc 𝐴 ) → 𝜑 )
63 1 2 3 isf32lem1 ( ( ( suc 𝐴 ∈ ω ∧ 𝑐 ∈ ω ) ∧ ( 𝑐 ⊆ suc 𝐴𝜑 ) ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
64 59 60 61 62 63 syl22anc ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) ∧ 𝑐 ⊆ suc 𝐴 ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
65 nnord ( suc 𝐴 ∈ ω → Ord suc 𝐴 )
66 6 65 syl ( 𝐴 ∈ ω → Ord suc 𝐴 )
67 66 ad2antlr ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) → Ord suc 𝐴 )
68 nnord ( 𝑐 ∈ ω → Ord 𝑐 )
69 68 ad2antll ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) → Ord 𝑐 )
70 ordtri2or2 ( ( Ord suc 𝐴 ∧ Ord 𝑐 ) → ( suc 𝐴𝑐𝑐 ⊆ suc 𝐴 ) )
71 67 69 70 syl2anc ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) → ( suc 𝐴𝑐𝑐 ⊆ suc 𝐴 ) )
72 58 64 71 mpjaodan ( ( ( 𝜑𝐴 ∈ ω ) ∧ ( ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ∧ 𝑐 ∈ ω ) ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
73 72 anassrs ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) ∧ 𝑐 ∈ ω ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) )
74 sseq2 ( ( 𝐹𝑐 ) = 𝑏 → ( ( 𝐹 ‘ suc 𝐴 ) ⊆ ( 𝐹𝑐 ) ↔ ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 ) )
75 73 74 syl5ibcom ( ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) ∧ 𝑐 ∈ ω ) → ( ( 𝐹𝑐 ) = 𝑏 → ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 ) )
76 75 rexlimdva ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ( ∃ 𝑐 ∈ ω ( 𝐹𝑐 ) = 𝑏 → ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 ) )
77 14 76 sylbid ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ( 𝑏 ∈ ran 𝐹 → ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 ) )
78 77 ralrimiv ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ∀ 𝑏 ∈ ran 𝐹 ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 )
79 ssint ( ( 𝐹 ‘ suc 𝐴 ) ⊆ ran 𝐹 ↔ ∀ 𝑏 ∈ ran 𝐹 ( 𝐹 ‘ suc 𝐴 ) ⊆ 𝑏 )
80 78 79 sylibr ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ( 𝐹 ‘ suc 𝐴 ) ⊆ ran 𝐹 )
81 11 80 eqssd ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ran 𝐹 = ( 𝐹 ‘ suc 𝐴 ) )
82 81 9 eqeltrd ( ( ( 𝜑𝐴 ∈ ω ) ∧ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ) → ran 𝐹 ∈ ran 𝐹 )
83 4 82 mtand ( ( 𝜑𝐴 ∈ ω ) → ¬ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
84 rexnal ( ∃ 𝑎 ∈ ω ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ↔ ¬ ∀ 𝑎 ∈ ω ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
85 83 84 sylibr ( ( 𝜑𝐴 ∈ ω ) → ∃ 𝑎 ∈ ω ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
86 suceq ( 𝑥 = 𝑎 → suc 𝑥 = suc 𝑎 )
87 86 fveq2d ( 𝑥 = 𝑎 → ( 𝐹 ‘ suc 𝑥 ) = ( 𝐹 ‘ suc 𝑎 ) )
88 fveq2 ( 𝑥 = 𝑎 → ( 𝐹𝑥 ) = ( 𝐹𝑎 ) )
89 87 88 sseq12d ( 𝑥 = 𝑎 → ( ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) ↔ ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) ) )
90 89 cbvralvw ( ∀ 𝑥 ∈ ω ( 𝐹 ‘ suc 𝑥 ) ⊆ ( 𝐹𝑥 ) ↔ ∀ 𝑎 ∈ ω ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) )
91 2 90 sylib ( 𝜑 → ∀ 𝑎 ∈ ω ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) )
92 91 adantr ( ( 𝜑𝐴 ∈ ω ) → ∀ 𝑎 ∈ ω ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) )
93 pm4.61 ( ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) ↔ ( 𝐴𝑎 ∧ ¬ ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
94 dfpss2 ( ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ↔ ( ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) ∧ ¬ ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) )
95 94 simplbi2 ( ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) → ( ¬ ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) → ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) )
96 95 anim2d ( ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) → ( ( 𝐴𝑎 ∧ ¬ ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) )
97 93 96 syl5bi ( ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) → ( ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) )
98 97 ralimi ( ∀ 𝑎 ∈ ω ( 𝐹 ‘ suc 𝑎 ) ⊆ ( 𝐹𝑎 ) → ∀ 𝑎 ∈ ω ( ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) )
99 rexim ( ∀ 𝑎 ∈ ω ( ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) → ( ∃ 𝑎 ∈ ω ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ∃ 𝑎 ∈ ω ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) )
100 92 98 99 3syl ( ( 𝜑𝐴 ∈ ω ) → ( ∃ 𝑎 ∈ ω ¬ ( 𝐴𝑎 → ( 𝐹 ‘ suc 𝑎 ) = ( 𝐹𝑎 ) ) → ∃ 𝑎 ∈ ω ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) ) )
101 85 100 mpd ( ( 𝜑𝐴 ∈ ω ) → ∃ 𝑎 ∈ ω ( 𝐴𝑎 ∧ ( 𝐹 ‘ suc 𝑎 ) ⊊ ( 𝐹𝑎 ) ) )