Proof of Theorem bnj1123
| Step | Hyp | Ref
| Expression |
| 1 | | bnj1123.2 |
. 2
⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) |
| 2 | | bnj1123.1 |
. . 3
⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
| 3 | 2 | sbcbii 3846 |
. 2
⊢
([𝑗 / 𝑖]𝜂 ↔ [𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
| 4 | | bnj1123.3 |
. . . . . . . 8
⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
| 5 | | nfcv 2905 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝐷 |
| 6 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖 𝑓 Fn 𝑛 |
| 7 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜑 |
| 8 | | bnj1123.4 |
. . . . . . . . . . . . 13
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
| 9 | 8 | bnj1095 34795 |
. . . . . . . . . . . 12
⊢ (𝜓 → ∀𝑖𝜓) |
| 10 | 9 | nf5i 2146 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜓 |
| 11 | 6, 7, 10 | nf3an 1901 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) |
| 12 | 5, 11 | nfrexw 3313 |
. . . . . . . . 9
⊢
Ⅎ𝑖∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) |
| 13 | 12 | nfab 2911 |
. . . . . . . 8
⊢
Ⅎ𝑖{𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
| 14 | 4, 13 | nfcxfr 2903 |
. . . . . . 7
⊢
Ⅎ𝑖𝐾 |
| 15 | 14 | nfcri 2897 |
. . . . . 6
⊢
Ⅎ𝑖 𝑓 ∈ 𝐾 |
| 16 | | nfv 1914 |
. . . . . 6
⊢
Ⅎ𝑖 𝑗 ∈ dom 𝑓 |
| 17 | 15, 16 | nfan 1899 |
. . . . 5
⊢
Ⅎ𝑖(𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) |
| 18 | | nfv 1914 |
. . . . 5
⊢
Ⅎ𝑖(𝑓‘𝑗) ⊆ 𝐵 |
| 19 | 17, 18 | nfim 1896 |
. . . 4
⊢
Ⅎ𝑖((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵) |
| 20 | | eleq1w 2824 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑖 ∈ dom 𝑓 ↔ 𝑗 ∈ dom 𝑓)) |
| 21 | 20 | anbi2d 630 |
. . . . 5
⊢ (𝑖 = 𝑗 → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ (𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓))) |
| 22 | | fveq2 6906 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑓‘𝑖) = (𝑓‘𝑗)) |
| 23 | 22 | sseq1d 4015 |
. . . . 5
⊢ (𝑖 = 𝑗 → ((𝑓‘𝑖) ⊆ 𝐵 ↔ (𝑓‘𝑗) ⊆ 𝐵)) |
| 24 | 21, 23 | imbi12d 344 |
. . . 4
⊢ (𝑖 = 𝑗 → (((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))) |
| 25 | 19, 24 | sbciegf 3827 |
. . 3
⊢ (𝑗 ∈ V → ([𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))) |
| 26 | 25 | elv 3485 |
. 2
⊢
([𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |
| 27 | 1, 3, 26 | 3bitri 297 |
1
⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |