Proof of Theorem isf32lem8
Step | Hyp | Ref
| Expression |
1 | | isf32lem.f |
. . . 4
⊢ 𝐾 = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽) |
2 | 1 | fveq1i 6104 |
. . 3
⊢ (𝐾‘𝐴) = (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) |
3 | | isf32lem.d |
. . . . . . . 8
⊢ 𝑆 = {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} |
4 | | ssrab2 3650 |
. . . . . . . 8
⊢ {𝑦 ∈ ω ∣ (𝐹‘suc 𝑦) ⊊ (𝐹‘𝑦)} ⊆ ω |
5 | 3, 4 | eqsstri 3598 |
. . . . . . 7
⊢ 𝑆 ⊆
ω |
6 | | isf32lem.a |
. . . . . . . 8
⊢ (𝜑 → 𝐹:ω⟶𝒫 𝐺) |
7 | | isf32lem.b |
. . . . . . . 8
⊢ (𝜑 → ∀𝑥 ∈ ω (𝐹‘suc 𝑥) ⊆ (𝐹‘𝑥)) |
8 | | isf32lem.c |
. . . . . . . 8
⊢ (𝜑 → ¬ ∩ ran 𝐹 ∈ ran 𝐹) |
9 | 6, 7, 8, 3 | isf32lem5 9062 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑆 ∈ Fin) |
10 | | isf32lem.e |
. . . . . . . 8
⊢ 𝐽 = (𝑢 ∈ ω ↦ (℩𝑣 ∈ 𝑆 (𝑣 ∩ 𝑆) ≈ 𝑢)) |
11 | 10 | fin23lem22 9032 |
. . . . . . 7
⊢ ((𝑆 ⊆ ω ∧ ¬
𝑆 ∈ Fin) → 𝐽:ω–1-1-onto→𝑆) |
12 | 5, 9, 11 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → 𝐽:ω–1-1-onto→𝑆) |
13 | | f1of 6050 |
. . . . . 6
⊢ (𝐽:ω–1-1-onto→𝑆 → 𝐽:ω⟶𝑆) |
14 | 12, 13 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐽:ω⟶𝑆) |
15 | | fvco3 6185 |
. . . . 5
⊢ ((𝐽:ω⟶𝑆 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
16 | 14, 15 | sylan 487 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴))) |
17 | 14 | ffvelrnda 6267 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐽‘𝐴) ∈ 𝑆) |
18 | | fveq2 6103 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘𝑤) = (𝐹‘(𝐽‘𝐴))) |
19 | | suceq 5707 |
. . . . . . . 8
⊢ (𝑤 = (𝐽‘𝐴) → suc 𝑤 = suc (𝐽‘𝐴)) |
20 | 19 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑤 = (𝐽‘𝐴) → (𝐹‘suc 𝑤) = (𝐹‘suc (𝐽‘𝐴))) |
21 | 18, 20 | difeq12d 3691 |
. . . . . 6
⊢ (𝑤 = (𝐽‘𝐴) → ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
22 | | eqid 2610 |
. . . . . 6
⊢ (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) = (𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) |
23 | | fvex 6113 |
. . . . . . 7
⊢ (𝐹‘(𝐽‘𝐴)) ∈ V |
24 | | difexg 4735 |
. . . . . . 7
⊢ ((𝐹‘(𝐽‘𝐴)) ∈ V → ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∈ V) |
25 | 23, 24 | ax-mp 5 |
. . . . . 6
⊢ ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ∈ V |
26 | 21, 22, 25 | fvmpt 6191 |
. . . . 5
⊢ ((𝐽‘𝐴) ∈ 𝑆 → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
27 | 17, 26 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤)))‘(𝐽‘𝐴)) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
28 | 16, 27 | eqtrd 2644 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (((𝑤 ∈ 𝑆 ↦ ((𝐹‘𝑤) ∖ (𝐹‘suc 𝑤))) ∘ 𝐽)‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
29 | 2, 28 | syl5eq 2656 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) = ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴)))) |
30 | 6 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → 𝐹:ω⟶𝒫 𝐺) |
31 | 5, 17 | sseldi 3566 |
. . . . 5
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐽‘𝐴) ∈ ω) |
32 | 30, 31 | ffvelrnd 6268 |
. . . 4
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐹‘(𝐽‘𝐴)) ∈ 𝒫 𝐺) |
33 | 32 | elpwid 4118 |
. . 3
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐹‘(𝐽‘𝐴)) ⊆ 𝐺) |
34 | 33 | ssdifssd 3710 |
. 2
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → ((𝐹‘(𝐽‘𝐴)) ∖ (𝐹‘suc (𝐽‘𝐴))) ⊆ 𝐺) |
35 | 29, 34 | eqsstrd 3602 |
1
⊢ ((𝜑 ∧ 𝐴 ∈ ω) → (𝐾‘𝐴) ⊆ 𝐺) |