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 𝑎 ) ⊊ ( 𝐹 ‘ 𝑎 ) ) )