| Step | Hyp | Ref
| Expression |
| 1 | | fveq2 6906 |
. . . . . 6
⊢ (𝑚 = ∅ → (𝐹‘𝑚) = (𝐹‘∅)) |
| 2 | | simpl2 1193 |
. . . . . . 7
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → 𝜑) |
| 3 | | bnj517.1 |
. . . . . . 7
⊢ (𝜑 ↔ (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) |
| 4 | 2, 3 | sylib 218 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → (𝐹‘∅) = pred(𝑋, 𝐴, 𝑅)) |
| 5 | 1, 4 | sylan9eqr 2799 |
. . . . 5
⊢ ((((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) ∧ 𝑚 = ∅) → (𝐹‘𝑚) = pred(𝑋, 𝐴, 𝑅)) |
| 6 | | bnj213 34896 |
. . . . 5
⊢
pred(𝑋, 𝐴, 𝑅) ⊆ 𝐴 |
| 7 | 5, 6 | eqsstrdi 4028 |
. . . 4
⊢ ((((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) ∧ 𝑚 = ∅) → (𝐹‘𝑚) ⊆ 𝐴) |
| 8 | | bnj517.2 |
. . . . . . 7
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 9 | | r19.29r 3116 |
. . . . . . . . . 10
⊢
((∃𝑖 ∈
ω 𝑚 = suc 𝑖 ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) → ∃𝑖 ∈ ω (𝑚 = suc 𝑖 ∧ (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
| 10 | | eleq1 2829 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ 𝑁 ↔ suc 𝑖 ∈ 𝑁)) |
| 11 | 10 | biimpd 229 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → (𝑚 ∈ 𝑁 → suc 𝑖 ∈ 𝑁)) |
| 12 | | fveqeq2 6915 |
. . . . . . . . . . . . . 14
⊢ (𝑚 = suc 𝑖 → ((𝐹‘𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 13 | | bnj213 34896 |
. . . . . . . . . . . . . . . . 17
⊢
pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
| 14 | 13 | rgenw 3065 |
. . . . . . . . . . . . . . . 16
⊢
∀𝑦 ∈
(𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
| 15 | | iunss 5045 |
. . . . . . . . . . . . . . . 16
⊢ (∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 ↔ ∀𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴) |
| 16 | 14, 15 | mpbir 231 |
. . . . . . . . . . . . . . 15
⊢ ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴 |
| 17 | | sseq1 4009 |
. . . . . . . . . . . . . . 15
⊢ ((𝐹‘𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) → ((𝐹‘𝑚) ⊆ 𝐴 ↔ ∪
𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) ⊆ 𝐴)) |
| 18 | 16, 17 | mpbiri 258 |
. . . . . . . . . . . . . 14
⊢ ((𝐹‘𝑚) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) → (𝐹‘𝑚) ⊆ 𝐴) |
| 19 | 12, 18 | biimtrrdi 254 |
. . . . . . . . . . . . 13
⊢ (𝑚 = suc 𝑖 → ((𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅) → (𝐹‘𝑚) ⊆ 𝐴)) |
| 20 | 11, 19 | imim12d 81 |
. . . . . . . . . . . 12
⊢ (𝑚 = suc 𝑖 → ((suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) → (𝑚 ∈ 𝑁 → (𝐹‘𝑚) ⊆ 𝐴))) |
| 21 | 20 | imp 406 |
. . . . . . . . . . 11
⊢ ((𝑚 = suc 𝑖 ∧ (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) → (𝑚 ∈ 𝑁 → (𝐹‘𝑚) ⊆ 𝐴)) |
| 22 | 21 | rexlimivw 3151 |
. . . . . . . . . 10
⊢
(∃𝑖 ∈
ω (𝑚 = suc 𝑖 ∧ (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) → (𝑚 ∈ 𝑁 → (𝐹‘𝑚) ⊆ 𝐴)) |
| 23 | 9, 22 | syl 17 |
. . . . . . . . 9
⊢
((∃𝑖 ∈
ω 𝑚 = suc 𝑖 ∧ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅))) → (𝑚 ∈ 𝑁 → (𝐹‘𝑚) ⊆ 𝐴)) |
| 24 | 23 | ex 412 |
. . . . . . . 8
⊢
(∃𝑖 ∈
ω 𝑚 = suc 𝑖 → (∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) → (𝑚 ∈ 𝑁 → (𝐹‘𝑚) ⊆ 𝐴))) |
| 25 | 24 | com3l 89 |
. . . . . . 7
⊢
(∀𝑖 ∈
ω (suc 𝑖 ∈ 𝑁 → (𝐹‘suc 𝑖) = ∪ 𝑦 ∈ (𝐹‘𝑖) pred(𝑦, 𝐴, 𝑅)) → (𝑚 ∈ 𝑁 → (∃𝑖 ∈ ω 𝑚 = suc 𝑖 → (𝐹‘𝑚) ⊆ 𝐴))) |
| 26 | 8, 25 | sylbi 217 |
. . . . . 6
⊢ (𝜓 → (𝑚 ∈ 𝑁 → (∃𝑖 ∈ ω 𝑚 = suc 𝑖 → (𝐹‘𝑚) ⊆ 𝐴))) |
| 27 | 26 | 3ad2ant3 1136 |
. . . . 5
⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → (𝑚 ∈ 𝑁 → (∃𝑖 ∈ ω 𝑚 = suc 𝑖 → (𝐹‘𝑚) ⊆ 𝐴))) |
| 28 | 27 | imp31 417 |
. . . 4
⊢ ((((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) ∧ ∃𝑖 ∈ ω 𝑚 = suc 𝑖) → (𝐹‘𝑚) ⊆ 𝐴) |
| 29 | | simpr 484 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ 𝑁) |
| 30 | | simpl1 1192 |
. . . . . 6
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → 𝑁 ∈ ω) |
| 31 | | elnn 7898 |
. . . . . 6
⊢ ((𝑚 ∈ 𝑁 ∧ 𝑁 ∈ ω) → 𝑚 ∈ ω) |
| 32 | 29, 30, 31 | syl2anc 584 |
. . . . 5
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → 𝑚 ∈ ω) |
| 33 | | nn0suc 7916 |
. . . . 5
⊢ (𝑚 ∈ ω → (𝑚 = ∅ ∨ ∃𝑖 ∈ ω 𝑚 = suc 𝑖)) |
| 34 | 32, 33 | syl 17 |
. . . 4
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → (𝑚 = ∅ ∨ ∃𝑖 ∈ ω 𝑚 = suc 𝑖)) |
| 35 | 7, 28, 34 | mpjaodan 961 |
. . 3
⊢ (((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) ∧ 𝑚 ∈ 𝑁) → (𝐹‘𝑚) ⊆ 𝐴) |
| 36 | 35 | ralrimiva 3146 |
. 2
⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑚 ∈ 𝑁 (𝐹‘𝑚) ⊆ 𝐴) |
| 37 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = 𝑛 → (𝐹‘𝑚) = (𝐹‘𝑛)) |
| 38 | 37 | sseq1d 4015 |
. . 3
⊢ (𝑚 = 𝑛 → ((𝐹‘𝑚) ⊆ 𝐴 ↔ (𝐹‘𝑛) ⊆ 𝐴)) |
| 39 | 38 | cbvralvw 3237 |
. 2
⊢
(∀𝑚 ∈
𝑁 (𝐹‘𝑚) ⊆ 𝐴 ↔ ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴) |
| 40 | 36, 39 | sylib 218 |
1
⊢ ((𝑁 ∈ ω ∧ 𝜑 ∧ 𝜓) → ∀𝑛 ∈ 𝑁 (𝐹‘𝑛) ⊆ 𝐴) |