Proof of Theorem bnj540
Step | Hyp | Ref
| Expression |
1 | | bnj540.2 |
. 2
⊢ (𝜓″ ↔ [𝐺 / 𝑓]𝜓) |
2 | | bnj540.1 |
. . . 4
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
3 | 2 | sbcbii 3775 |
. . 3
⊢
([𝐺 / 𝑓]𝜓 ↔ [𝐺 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
4 | | bnj540.3 |
. . . 4
⊢ 𝐺 ∈ V |
5 | 4 | bnj538 32728 |
. . 3
⊢
([𝐺 / 𝑓]∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖 ∈ ω [𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
6 | | sbcimg 3766 |
. . . . 5
⊢ (𝐺 ∈ V → ([𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)))) |
7 | 4, 6 | ax-mp 5 |
. . . 4
⊢
([𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
8 | 7 | ralbii 3091 |
. . 3
⊢
(∀𝑖 ∈
ω [𝐺 / 𝑓](suc 𝑖 ∈ 𝑁 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖 ∈ ω ([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
9 | 3, 5, 8 | 3bitri 297 |
. 2
⊢
([𝐺 / 𝑓]𝜓 ↔ ∀𝑖 ∈ ω ([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
10 | 4 | bnj525 32726 |
. . . 4
⊢
([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 ↔ suc 𝑖 ∈ 𝑁) |
11 | | fveq1 6765 |
. . . . . 6
⊢ (𝑓 = 𝐺 → (𝑓‘suc 𝑖) = (𝐺‘suc 𝑖)) |
12 | | fveq1 6765 |
. . . . . . 7
⊢ (𝑓 = 𝐺 → (𝑓‘𝑖) = (𝐺‘𝑖)) |
13 | 12 | bnj1113 32773 |
. . . . . 6
⊢ (𝑓 = 𝐺 → ∪
𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) = ∪
𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
14 | 11, 13 | eqeq12d 2754 |
. . . . 5
⊢ (𝑓 = 𝐺 → ((𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
15 | 4, 14 | sbcie 3758 |
. . . 4
⊢
([𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅) ↔ (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅)) |
16 | 10, 15 | imbi12i 351 |
. . 3
⊢
(([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
17 | 16 | ralbii 3091 |
. 2
⊢
(∀𝑖 ∈
ω ([𝐺 / 𝑓]suc 𝑖 ∈ 𝑁 → [𝐺 / 𝑓](𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅)) ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
18 | 1, 9, 17 | 3bitri 297 |
1
⊢ (𝜓″ ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑁 → (𝐺‘suc 𝑖) = ∪ 𝑦 ∈ (𝐺‘𝑖) pred(𝑦, 𝐴, 𝑅))) |