Step | Hyp | Ref
| Expression |
1 | | unblem.2 |
. . . . . . 7
⊢ 𝐹 = (rec((𝑥 ∈ V ↦ ∩ (𝐴
∖ suc 𝑥)), ∩ 𝐴)
↾ ω) |
2 | 1 | unblem2 8098 |
. . . . . 6
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ 𝐴)) |
3 | 2 | imp 444 |
. . . . 5
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → (𝐹‘𝑧) ∈ 𝐴) |
4 | | omsson 6961 |
. . . . . . . 8
⊢ ω
⊆ On |
5 | | sstr 3576 |
. . . . . . . 8
⊢ ((𝐴 ⊆ ω ∧ ω
⊆ On) → 𝐴
⊆ On) |
6 | 4, 5 | mpan2 703 |
. . . . . . 7
⊢ (𝐴 ⊆ ω → 𝐴 ⊆ On) |
7 | | ssel 3562 |
. . . . . . . 8
⊢ (𝐴 ⊆ On → ((𝐹‘𝑧) ∈ 𝐴 → (𝐹‘𝑧) ∈ On)) |
8 | 7 | anc2li 578 |
. . . . . . 7
⊢ (𝐴 ⊆ On → ((𝐹‘𝑧) ∈ 𝐴 → (𝐴 ⊆ On ∧ (𝐹‘𝑧) ∈ On))) |
9 | 6, 8 | syl 17 |
. . . . . 6
⊢ (𝐴 ⊆ ω → ((𝐹‘𝑧) ∈ 𝐴 → (𝐴 ⊆ On ∧ (𝐹‘𝑧) ∈ On))) |
10 | 9 | ad2antrr 758 |
. . . . 5
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → ((𝐹‘𝑧) ∈ 𝐴 → (𝐴 ⊆ On ∧ (𝐹‘𝑧) ∈ On))) |
11 | 3, 10 | mpd 15 |
. . . 4
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → (𝐴 ⊆ On ∧ (𝐹‘𝑧) ∈ On)) |
12 | | onmindif 5732 |
. . . 4
⊢ ((𝐴 ⊆ On ∧ (𝐹‘𝑧) ∈ On) → (𝐹‘𝑧) ∈ ∩ (𝐴 ∖ suc (𝐹‘𝑧))) |
13 | 11, 12 | syl 17 |
. . 3
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → (𝐹‘𝑧) ∈ ∩ (𝐴 ∖ suc (𝐹‘𝑧))) |
14 | | unblem1 8097 |
. . . . . . 7
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ (𝐹‘𝑧) ∈ 𝐴) → ∩ (𝐴 ∖ suc (𝐹‘𝑧)) ∈ 𝐴) |
15 | 14 | ex 449 |
. . . . . 6
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → ((𝐹‘𝑧) ∈ 𝐴 → ∩ (𝐴 ∖ suc (𝐹‘𝑧)) ∈ 𝐴)) |
16 | 2, 15 | syld 46 |
. . . . 5
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → ∩ (𝐴
∖ suc (𝐹‘𝑧)) ∈ 𝐴)) |
17 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑦 = 𝑥 → suc 𝑦 = suc 𝑥) |
18 | 17 | difeq2d 3690 |
. . . . . . . 8
⊢ (𝑦 = 𝑥 → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc 𝑥)) |
19 | 18 | inteqd 4415 |
. . . . . . 7
⊢ (𝑦 = 𝑥 → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc 𝑥)) |
20 | | suceq 5707 |
. . . . . . . . 9
⊢ (𝑦 = (𝐹‘𝑧) → suc 𝑦 = suc (𝐹‘𝑧)) |
21 | 20 | difeq2d 3690 |
. . . . . . . 8
⊢ (𝑦 = (𝐹‘𝑧) → (𝐴 ∖ suc 𝑦) = (𝐴 ∖ suc (𝐹‘𝑧))) |
22 | 21 | inteqd 4415 |
. . . . . . 7
⊢ (𝑦 = (𝐹‘𝑧) → ∩ (𝐴 ∖ suc 𝑦) = ∩ (𝐴 ∖ suc (𝐹‘𝑧))) |
23 | 1, 19, 22 | frsucmpt2 7422 |
. . . . . 6
⊢ ((𝑧 ∈ ω ∧ ∩ (𝐴
∖ suc (𝐹‘𝑧)) ∈ 𝐴) → (𝐹‘suc 𝑧) = ∩ (𝐴 ∖ suc (𝐹‘𝑧))) |
24 | 23 | ex 449 |
. . . . 5
⊢ (𝑧 ∈ ω → (∩ (𝐴
∖ suc (𝐹‘𝑧)) ∈ 𝐴 → (𝐹‘suc 𝑧) = ∩ (𝐴 ∖ suc (𝐹‘𝑧)))) |
25 | 16, 24 | sylcom 30 |
. . . 4
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘suc 𝑧) = ∩ (𝐴 ∖ suc (𝐹‘𝑧)))) |
26 | 25 | imp 444 |
. . 3
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → (𝐹‘suc 𝑧) = ∩ (𝐴 ∖ suc (𝐹‘𝑧))) |
27 | 13, 26 | eleqtrrd 2691 |
. 2
⊢ (((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) ∧ 𝑧 ∈ ω) → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧)) |
28 | 27 | ex 449 |
1
⊢ ((𝐴 ⊆ ω ∧
∀𝑤 ∈ ω
∃𝑣 ∈ 𝐴 𝑤 ∈ 𝑣) → (𝑧 ∈ ω → (𝐹‘𝑧) ∈ (𝐹‘suc 𝑧))) |