Step | Hyp | Ref
| Expression |
1 | | isf32lem.c |
. . . . 5
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
2 | 1 | adantr 480 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
3 | | isf32lem.a |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
4 | | ffn 5958 |
. . . . . . . . . 10
⊢ (𝐹:ω⟶𝒫 𝐺 → 𝐹 Fn ω) |
5 | 3, 4 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝐹 Fn ω) |
6 | | peano2 6978 |
. . . . . . . . 9
⊢ (𝐴 ∈ ω → suc 𝐴 ∈
ω) |
7 | | fnfvelrn 6264 |
. . . . . . . . 9
⊢ ((𝐹 Fn ω ∧ suc 𝐴 ∈ ω) → (𝐹‘suc 𝐴) ∈ ran 𝐹) |
8 | 5, 6, 7 | syl2an 493 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐹‘suc 𝐴) ∈ ran 𝐹) |
9 | 8 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → (𝐹‘suc 𝐴) ∈ ran 𝐹) |
10 | | intss1 4427 |
. . . . . . 7
⊢ ((𝐹‘suc 𝐴) ∈ ran 𝐹 → ∩ ran
𝐹 ⊆ (𝐹‘suc 𝐴)) |
11 | 9, 10 | syl 17 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → ∩ ran
𝐹 ⊆ (𝐹‘suc 𝐴)) |
12 | | fvelrnb 6153 |
. . . . . . . . . . 11
⊢ (𝐹 Fn ω → (𝑏 ∈ ran 𝐹 ↔ ∃𝑐 ∈ ω (𝐹‘𝑐) = 𝑏)) |
13 | 5, 12 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑏 ∈ ran 𝐹 ↔ ∃𝑐 ∈ ω (𝐹‘𝑐) = 𝑏)) |
14 | 13 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → (𝑏 ∈ ran 𝐹 ↔ ∃𝑐 ∈ ω (𝐹‘𝑐) = 𝑏)) |
15 | | simplrr 797 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → 𝑐 ∈ ω) |
16 | 6 | ad3antlr 763 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → suc 𝐴 ∈ ω) |
17 | | simpr 476 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → suc 𝐴 ⊆ 𝑐) |
18 | | simplrl 796 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
19 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = suc 𝐴 → (𝐹‘𝑏) = (𝐹‘suc 𝐴)) |
20 | 19 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = suc 𝐴 → ((𝐹‘suc 𝐴) = (𝐹‘𝑏) ↔ (𝐹‘suc 𝐴) = (𝐹‘suc 𝐴))) |
21 | 20 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = suc 𝐴 → ((∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑏)) ↔ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝐴)))) |
22 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑑 → (𝐹‘𝑏) = (𝐹‘𝑑)) |
23 | 22 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑑 → ((𝐹‘suc 𝐴) = (𝐹‘𝑏) ↔ (𝐹‘suc 𝐴) = (𝐹‘𝑑))) |
24 | 23 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑑 → ((∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑏)) ↔ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑑)))) |
25 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = suc 𝑑 → (𝐹‘𝑏) = (𝐹‘suc 𝑑)) |
26 | 25 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = suc 𝑑 → ((𝐹‘suc 𝐴) = (𝐹‘𝑏) ↔ (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑))) |
27 | 26 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = suc 𝑑 → ((∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑏)) ↔ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑)))) |
28 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑏 = 𝑐 → (𝐹‘𝑏) = (𝐹‘𝑐)) |
29 | 28 | eqeq2d 2620 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 = 𝑐 → ((𝐹‘suc 𝐴) = (𝐹‘𝑏) ↔ (𝐹‘suc 𝐴) = (𝐹‘𝑐))) |
30 | 29 | imbi2d 329 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑏 = 𝑐 → ((∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑏)) ↔ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑐)))) |
31 | | eqid 2610 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝐹‘suc 𝐴) = (𝐹‘suc 𝐴) |
32 | 31 | 2a1i 12 |
. . . . . . . . . . . . . . . . 17
⊢ (suc
𝐴 ∈ ω →
(∀𝑎 ∈ ω
(𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝐴))) |
33 | | elex 3185 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (suc
𝐴 ∈ ω → suc
𝐴 ∈
V) |
34 | | sucexb 6901 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝐴 ∈ V ↔ suc 𝐴 ∈ V) |
35 | 33, 34 | sylibr 223 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (suc
𝐴 ∈ ω →
𝐴 ∈
V) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) → 𝐴 ∈ V) |
37 | | sucssel 5736 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐴 ∈ V → (suc 𝐴 ⊆ 𝑑 → 𝐴 ∈ 𝑑)) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) → (suc
𝐴 ⊆ 𝑑 → 𝐴 ∈ 𝑑)) |
39 | 38 | imp 444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑑) → 𝐴 ∈ 𝑑) |
40 | | eleq2 2677 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑑 → (𝐴 ∈ 𝑎 ↔ 𝐴 ∈ 𝑑)) |
41 | | suceq 5707 |
. . . . . . . . . . . . . . . . . . . . . . . . . 26
⊢ (𝑎 = 𝑑 → suc 𝑎 = suc 𝑑) |
42 | 41 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑑 → (𝐹‘suc 𝑎) = (𝐹‘suc 𝑑)) |
43 | | fveq2 6103 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑎 = 𝑑 → (𝐹‘𝑎) = (𝐹‘𝑑)) |
44 | 42, 43 | eqeq12d 2625 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑎 = 𝑑 → ((𝐹‘suc 𝑎) = (𝐹‘𝑎) ↔ (𝐹‘suc 𝑑) = (𝐹‘𝑑))) |
45 | 40, 44 | imbi12d 333 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑎 = 𝑑 → ((𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ↔ (𝐴 ∈ 𝑑 → (𝐹‘suc 𝑑) = (𝐹‘𝑑)))) |
46 | 45 | rspcv 3278 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑑 ∈ ω →
(∀𝑎 ∈ ω
(𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐴 ∈ 𝑑 → (𝐹‘suc 𝑑) = (𝐹‘𝑑)))) |
47 | 46 | com23 84 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑑 ∈ ω → (𝐴 ∈ 𝑑 → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝑑) = (𝐹‘𝑑)))) |
48 | 47 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑑) → (𝐴 ∈ 𝑑 → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝑑) = (𝐹‘𝑑)))) |
49 | 39, 48 | mpd 15 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑑) → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝑑) = (𝐹‘𝑑))) |
50 | | eqtr3 2631 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝐹‘suc 𝐴) = (𝐹‘𝑑) ∧ (𝐹‘suc 𝑑) = (𝐹‘𝑑)) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑)) |
51 | 50 | expcom 450 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝐹‘suc 𝑑) = (𝐹‘𝑑) → ((𝐹‘suc 𝐴) = (𝐹‘𝑑) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑))) |
52 | 49, 51 | syl6 34 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑑) → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → ((𝐹‘suc 𝐴) = (𝐹‘𝑑) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑)))) |
53 | 52 | a2d 29 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑑 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑑) → ((∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑑)) → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘suc 𝑑)))) |
54 | 21, 24, 27, 30, 32, 53 | findsg 6985 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑐 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ suc 𝐴 ⊆ 𝑐) → (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐹‘suc 𝐴) = (𝐹‘𝑐))) |
55 | 54 | impr 647 |
. . . . . . . . . . . . . . 15
⊢ (((𝑐 ∈ ω ∧ suc 𝐴 ∈ ω) ∧ (suc
𝐴 ⊆ 𝑐 ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)))) → (𝐹‘suc 𝐴) = (𝐹‘𝑐)) |
56 | 15, 16, 17, 18, 55 | syl22anc 1319 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → (𝐹‘suc 𝐴) = (𝐹‘𝑐)) |
57 | | eqimss 3620 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘suc 𝐴) = (𝐹‘𝑐) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
58 | 56, 57 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ suc 𝐴 ⊆ 𝑐) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
59 | 6 | ad3antlr 763 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ 𝑐 ⊆ suc 𝐴) → suc 𝐴 ∈ ω) |
60 | | simplrr 797 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ 𝑐 ⊆ suc 𝐴) → 𝑐 ∈ ω) |
61 | | simpr 476 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ 𝑐 ⊆ suc 𝐴) → 𝑐 ⊆ suc 𝐴) |
62 | | simplll 794 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ 𝑐 ⊆ suc 𝐴) → 𝜑) |
63 | | isf32lem.b |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
64 | 3, 63, 1 | isf32lem1 9058 |
. . . . . . . . . . . . . 14
⊢ (((suc
𝐴 ∈ ω ∧
𝑐 ∈ ω) ∧
(𝑐 ⊆ suc 𝐴 ∧ 𝜑)) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
65 | 59, 60, 61, 62, 64 | syl22anc 1319 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) ∧ 𝑐 ⊆ suc 𝐴) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
66 | | nnord 6965 |
. . . . . . . . . . . . . . . 16
⊢ (suc
𝐴 ∈ ω → Ord
suc 𝐴) |
67 | 6, 66 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝐴 ∈ ω → Ord suc
𝐴) |
68 | 67 | ad2antlr 759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) → Ord suc 𝐴) |
69 | | nnord 6965 |
. . . . . . . . . . . . . . 15
⊢ (𝑐 ∈ ω → Ord 𝑐) |
70 | 69 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) → Ord 𝑐) |
71 | | ordtri2or2 5740 |
. . . . . . . . . . . . . 14
⊢ ((Ord suc
𝐴 ∧ Ord 𝑐) → (suc 𝐴 ⊆ 𝑐 ∨ 𝑐 ⊆ suc 𝐴)) |
72 | 68, 70, 71 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) → (suc 𝐴 ⊆ 𝑐 ∨ 𝑐 ⊆ suc 𝐴)) |
73 | 58, 65, 72 | mpjaodan 823 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ (∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ∧ 𝑐 ∈ ω)) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
74 | 73 | anassrs 678 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) ∧ 𝑐 ∈ ω) → (𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐)) |
75 | | sseq2 3590 |
. . . . . . . . . . 11
⊢ ((𝐹‘𝑐) = 𝑏 → ((𝐹‘suc 𝐴) ⊆ (𝐹‘𝑐) ↔ (𝐹‘suc 𝐴) ⊆ 𝑏)) |
76 | 74, 75 | syl5ibcom 234 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) ∧ 𝑐 ∈ ω) → ((𝐹‘𝑐) = 𝑏 → (𝐹‘suc 𝐴) ⊆ 𝑏)) |
77 | 76 | rexlimdva 3013 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → (∃𝑐 ∈ ω (𝐹‘𝑐) = 𝑏 → (𝐹‘suc 𝐴) ⊆ 𝑏)) |
78 | 14, 77 | sylbid 229 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → (𝑏 ∈ ran 𝐹 → (𝐹‘suc 𝐴) ⊆ 𝑏)) |
79 | 78 | ralrimiv 2948 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → ∀𝑏 ∈ ran 𝐹(𝐹‘suc 𝐴) ⊆ 𝑏) |
80 | | ssint 4428 |
. . . . . . 7
⊢ ((𝐹‘suc 𝐴) ⊆ ∩ ran
𝐹 ↔ ∀𝑏 ∈ ran 𝐹(𝐹‘suc 𝐴) ⊆ 𝑏) |
81 | 79, 80 | sylibr 223 |
. . . . . 6
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → (𝐹‘suc 𝐴) ⊆ ∩ ran
𝐹) |
82 | 11, 81 | eqssd 3585 |
. . . . 5
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → ∩ ran
𝐹 = (𝐹‘suc 𝐴)) |
83 | 82, 9 | eqeltrd 2688 |
. . . 4
⊢ (((𝜑 ∧ 𝐴 ∈ ω) ∧ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) → ∩ ran
𝐹 ∈ ran 𝐹) |
84 | 2, 83 | mtand 689 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ¬ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
85 | | rexnal 2978 |
. . 3
⊢
(∃𝑎 ∈
ω ¬ (𝐴 ∈
𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ↔ ¬ ∀𝑎 ∈ ω (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
86 | 84, 85 | sylibr 223 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∃𝑎 ∈ ω ¬ (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
87 | | suceq 5707 |
. . . . . . . 8
⊢ (𝑥 = 𝑎 → suc 𝑥 = suc 𝑎) |
88 | 87 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝐹‘suc 𝑥) = (𝐹‘suc 𝑎)) |
89 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑥 = 𝑎 → (𝐹‘𝑥) = (𝐹‘𝑎)) |
90 | 88, 89 | sseq12d 3597 |
. . . . . 6
⊢ (𝑥 = 𝑎 → ((𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥) ↔ (𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎))) |
91 | 90 | cbvralv 3147 |
. . . . 5
⊢
(∀𝑥 ∈
ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥) ↔ ∀𝑎 ∈ ω (𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎)) |
92 | 63, 91 | sylib 207 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ ω (𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎)) |
93 | 92 | adantr 480 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∀𝑎 ∈ ω (𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎)) |
94 | | pm4.61 441 |
. . . . 5
⊢ (¬
(𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) ↔ (𝐴 ∈ 𝑎 ∧ ¬ (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
95 | | dfpss2 3654 |
. . . . . . 7
⊢ ((𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎) ↔ ((𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎) ∧ ¬ (𝐹‘suc 𝑎) = (𝐹‘𝑎))) |
96 | 95 | simplbi2 653 |
. . . . . 6
⊢ ((𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎) → (¬ (𝐹‘suc 𝑎) = (𝐹‘𝑎) → (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎))) |
97 | 96 | anim2d 587 |
. . . . 5
⊢ ((𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎) → ((𝐴 ∈ 𝑎 ∧ ¬ (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))) |
98 | 94, 97 | syl5bi 231 |
. . . 4
⊢ ((𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎) → (¬ (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))) |
99 | 98 | ralimi 2936 |
. . 3
⊢
(∀𝑎 ∈
ω (𝐹‘suc 𝑎) ⊆ (𝐹‘𝑎) → ∀𝑎 ∈ ω (¬ (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))) |
100 | | rexim 2991 |
. . 3
⊢
(∀𝑎 ∈
ω (¬ (𝐴 ∈
𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎))) → (∃𝑎 ∈ ω ¬ (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))) |
101 | 93, 99, 100 | 3syl 18 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (∃𝑎 ∈ ω ¬ (𝐴 ∈ 𝑎 → (𝐹‘suc 𝑎) = (𝐹‘𝑎)) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎)))) |
102 | 86, 101 | mpd 15 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ∃𝑎 ∈ ω (𝐴 ∈ 𝑎 ∧ (𝐹‘suc 𝑎) ⊊ (𝐹‘𝑎))) |