| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = ∅ → (𝐹‘𝑧) = (𝐹‘∅)) |
| 2 | 1 | eleq1d 2826 |
. . 3
⊢ (𝑧 = ∅ → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘∅) ∈ 𝐴)) |
| 3 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = 𝑢 → (𝐹‘𝑧) = (𝐹‘𝑢)) |
| 4 | 3 | eleq1d 2826 |
. . 3
⊢ (𝑧 = 𝑢 → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘𝑢) ∈ 𝐴)) |
| 5 | | fveq2 6906 |
. . . 4
⊢ (𝑧 = suc 𝑢 → (𝐹‘𝑧) = (𝐹‘suc 𝑢)) |
| 6 | 5 | eleq1d 2826 |
. . 3
⊢ (𝑧 = suc 𝑢 → ((𝐹‘𝑧) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴)) |
| 7 | | omsson 7891 |
. . . . . 6
⊢ ω
⊆ On |
| 8 | | sstr 3992 |
. . . . . 6
⊢ ((𝐴 ⊆ ω ∧ ω
⊆ On) → 𝐴
⊆ On) |
| 9 | 7, 8 | mpan2 691 |
. . . . 5
⊢ (𝐴 ⊆ ω → 𝐴 ⊆ On) |
| 10 | | peano1 7910 |
. . . . . . . . 9
⊢ ∅
∈ ω |
| 11 | | eleq1 2829 |
. . . . . . . . . . 11
⊢ (𝑤 = ∅ → (𝑤 ∈ 𝑣 ↔ ∅ ∈ 𝑣)) |
| 12 | 11 | rexbidv 3179 |
. . . . . . . . . 10
⊢ (𝑤 = ∅ → (∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 ↔ ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣)) |
| 13 | 12 | rspcv 3618 |
. . . . . . . . 9
⊢ (∅
∈ ω → (∀𝑤 ∈ ω ∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣 → ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣)) |
| 14 | 10, 13 | ax-mp 5 |
. . . . . . . 8
⊢
(∀𝑤 ∈
ω ∃𝑣 ∈
𝐴 𝑤 ∈ 𝑣 → ∃𝑣 ∈ 𝐴 ∅ ∈ 𝑣) |
| 15 | | df-rex 3071 |
. . . . . . . 8
⊢
(∃𝑣 ∈
𝐴 ∅ ∈ 𝑣 ↔ ∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣)) |
| 16 | 14, 15 | sylib 218 |
. . . . . . 7
⊢
(∀𝑤 ∈
ω ∃𝑣 ∈
𝐴 𝑤 ∈ 𝑣 → ∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣)) |
| 17 | | exsimpl 1868 |
. . . . . . 7
⊢
(∃𝑣(𝑣 ∈ 𝐴 ∧ ∅ ∈ 𝑣) → ∃𝑣 𝑣 ∈ 𝐴) |
| 18 | 16, 17 | syl 17 |
. . . . . 6
⊢
(∀𝑤 ∈
ω ∃𝑣 ∈
𝐴 𝑤 ∈ 𝑣 → ∃𝑣 𝑣 ∈ 𝐴) |
| 19 | | n0 4353 |
. . . . . 6
⊢ (𝐴 ≠ ∅ ↔
∃𝑣 𝑣 ∈ 𝐴) |
| 20 | 18, 19 | sylibr 234 |
. . . . 5
⊢
(∀𝑤 ∈
ω ∃𝑣 ∈
𝐴 𝑤 ∈ 𝑣 → 𝐴 ≠ ∅) |
| 21 | | onint 7810 |
. . . . 5
⊢ ((𝐴 ⊆ On ∧ 𝐴 ≠ ∅) → ∩ 𝐴
∈ 𝐴) |
| 22 | 9, 20, 21 | syl2an 596 |
. . . 4
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → ∩ 𝐴 ∈ 𝐴) |
| 23 | | unblem.2 |
. . . . . . . 8
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴
∖ suc 𝑥)), ∩ 𝐴)
↾ ω) |
| 24 | 23 | fveq1i 6907 |
. . . . . . 7
⊢ (𝐹‘∅) = ((rec((𝑥 ∈ V ↦ ∩ (𝐴
∖ suc 𝑥)), ∩ 𝐴)
↾ ω)‘∅) |
| 25 | | fr0g 8476 |
. . . . . . 7
⊢ (∩ 𝐴
∈ 𝐴 →
((rec((𝑥 ∈ V ↦
∩ (𝐴 ∖ suc 𝑥)), ∩ 𝐴) ↾
ω)‘∅) = ∩ 𝐴) |
| 26 | 24, 25 | eqtr2id 2790 |
. . . . . 6
⊢ (∩ 𝐴
∈ 𝐴 → ∩ 𝐴 =
(𝐹‘∅)) |
| 27 | 26 | eleq1d 2826 |
. . . . 5
⊢ (∩ 𝐴
∈ 𝐴 → (∩ 𝐴
∈ 𝐴 ↔ (𝐹‘∅) ∈ 𝐴)) |
| 28 | 27 | ibi 267 |
. . . 4
⊢ (∩ 𝐴
∈ 𝐴 → (𝐹‘∅) ∈ 𝐴) |
| 29 | 22, 28 | syl 17 |
. . 3
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝐹‘∅) ∈ 𝐴) |
| 30 | | unblem1 9328 |
. . . . 5
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ (𝐹‘𝑢) ∈ 𝐴) → ∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴) |
| 31 | | suceq 6450 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑥 → suc 𝑦 = suc 𝑥) |
| 32 | 31 | difeq2d 4126 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑥 → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc 𝑥)) |
| 33 | 32 | inteqd 4951 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑥 → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc 𝑥)) |
| 34 | | suceq 6450 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝐹‘𝑢) → suc 𝑦 = suc (𝐹‘𝑢)) |
| 35 | 34 | difeq2d 4126 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝐹‘𝑢) → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc (𝐹‘𝑢))) |
| 36 | 35 | inteqd 4951 |
. . . . . . . . . 10
⊢ (𝑦 = (𝐹‘𝑢) → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc (𝐹‘𝑢))) |
| 37 | 23, 33, 36 | frsucmpt2 8480 |
. . . . . . . . 9
⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴
∖ suc (𝐹‘𝑢)) ∈ 𝐴) → (𝐹‘suc 𝑢) = ∩ (𝐴 ∖ suc (𝐹‘𝑢))) |
| 38 | 37 | eqcomd 2743 |
. . . . . . . 8
⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴
∖ suc (𝐹‘𝑢)) ∈ 𝐴) → ∩ (𝐴 ∖ suc (𝐹‘𝑢)) = (𝐹‘suc 𝑢)) |
| 39 | 38 | eleq1d 2826 |
. . . . . . 7
⊢ ((𝑢 ∈ ω ∧ ∩ (𝐴
∖ suc (𝐹‘𝑢)) ∈ 𝐴) → (∩
(𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴)) |
| 40 | 39 | ex 412 |
. . . . . 6
⊢ (𝑢 ∈ ω → (∩ (𝐴
∖ suc (𝐹‘𝑢)) ∈ 𝐴 → (∩ (𝐴 ∖ suc (𝐹‘𝑢)) ∈ 𝐴 ↔ (𝐹‘suc 𝑢) ∈ 𝐴))) |
| 41 | 40 | ibd 269 |
. . . . 5
⊢ (𝑢 ∈ ω → (∩ (𝐴
∖ suc (𝐹‘𝑢)) ∈ 𝐴 → (𝐹‘suc 𝑢) ∈ 𝐴)) |
| 42 | 30, 41 | syl5 34 |
. . . 4
⊢ (𝑢 ∈ ω → (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ (𝐹‘𝑢) ∈ 𝐴) → (𝐹‘suc 𝑢) ∈ 𝐴)) |
| 43 | 42 | expd 415 |
. . 3
⊢ (𝑢 ∈ ω → ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → ((𝐹‘𝑢) ∈ 𝐴 → (𝐹‘suc 𝑢) ∈ 𝐴))) |
| 44 | 2, 4, 6, 29, 43 | finds2 7920 |
. 2
⊢ (𝑧 ∈ ω → ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝐹‘𝑧) ∈ 𝐴)) |
| 45 | 44 | com12 32 |
1
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) |