Proof of Theorem bnj999
Step | Hyp | Ref
| Expression |
1 | | bnj999.3 |
. . . . . . 7
⊢ (𝜒 ↔ (𝑛 ∈ 𝐷 ∧ 𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)) |
2 | | bnj999.7 |
. . . . . . 7
⊢ (𝜑′ ↔ [𝑝 / 𝑛]𝜑) |
3 | | bnj999.8 |
. . . . . . 7
⊢ (𝜓′ ↔ [𝑝 / 𝑛]𝜓) |
4 | | bnj999.9 |
. . . . . . 7
⊢ (𝜒′ ↔ [𝑝 / 𝑛]𝜒) |
5 | | vex 3412 |
. . . . . . 7
⊢ 𝑝 ∈ V |
6 | 1, 2, 3, 4, 5 | bnj919 32459 |
. . . . . 6
⊢ (𝜒′ ↔ (𝑝 ∈ 𝐷 ∧ 𝑓 Fn 𝑝 ∧ 𝜑′ ∧ 𝜓′)) |
7 | | bnj999.10 |
. . . . . 6
⊢ (𝜑″ ↔ [𝐺 / 𝑓]𝜑′) |
8 | | bnj999.11 |
. . . . . 6
⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓′) |
9 | | bnj999.12 |
. . . . . 6
⊢ (𝜒″ ↔ [𝐺 / 𝑓]𝜒′) |
10 | | bnj999.16 |
. . . . . . 7
⊢ 𝐺 = (𝑓 ∪ {〈𝑛, 𝐶〉}) |
11 | 10 | bnj918 32458 |
. . . . . 6
⊢ 𝐺 ∈ V |
12 | 6, 7, 8, 9, 11 | bnj976 32470 |
. . . . 5
⊢ (𝜒″ ↔ (𝑝 ∈ 𝐷 ∧ 𝐺 Fn 𝑝 ∧ 𝜑″ ∧ 𝜓″)) |
13 | 12 | bnj1254 32502 |
. . . 4
⊢ (𝜒″ → 𝜓″) |
14 | 13 | anim1i 618 |
. . 3
⊢ ((𝜒″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖))) → (𝜓″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) |
15 | | bnj252 32394 |
. . 3
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) ↔ (𝜒″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) |
16 | | bnj252 32394 |
. . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) ↔ (𝜓″ ∧ (𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)))) |
17 | 14, 15, 16 | 3imtr4i 295 |
. 2
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → (𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖))) |
18 | | ssiun2 4956 |
. . . 4
⊢ (𝑦 ∈ (𝐺‘𝑖) → pred(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
19 | 18 | bnj708 32448 |
. . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
20 | | 3simpa 1150 |
. . . . . 6
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝜓″ ∧ 𝑖 ∈ ω)) |
21 | 20 | ancomd 465 |
. . . . 5
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝑖 ∈ ω ∧ 𝜓″)) |
22 | | simp3 1140 |
. . . . 5
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → suc 𝑖 ∈ 𝑝) |
23 | | bnj999.2 |
. . . . . . . 8
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
24 | 23, 3, 5 | bnj539 32584 |
. . . . . . 7
⊢ (𝜓′ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑝 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
25 | | bnj999.15 |
. . . . . . 7
⊢ 𝐶 = ∪ 𝑦 ∈ (𝑓‘𝑚) pred(𝑦, 𝐴, 𝑅) |
26 | 24, 8, 25, 10 | bnj965 32635 |
. . . . . 6
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑝 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
27 | 26 | bnj228 32426 |
. . . . 5
⊢ ((𝑖 ∈ ω ∧ 𝜓″) → (suc 𝑖 ∈ 𝑝 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
28 | 21, 22, 27 | sylc 65 |
. . . 4
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
29 | 28 | bnj721 32449 |
. . 3
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
30 | 19, 29 | sseqtrrd 3942 |
. 2
⊢ ((𝜓″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) |
31 | 17, 30 | syl 17 |
1
⊢ ((𝜒″ ∧ 𝑖 ∈ ω ∧ suc 𝑖 ∈ 𝑝 ∧ 𝑦 ∈ (𝐺‘𝑖)) → pred(𝑦, 𝐴, 𝑅) ⊆ (𝐺‘suc 𝑖)) |