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