Proof of Theorem bnj1123
Step | Hyp | Ref
| Expression |
1 | | bnj1123.2 |
. 2
⊢ (𝜂′ ↔ [𝑗 / 𝑖]𝜂) |
2 | | bnj1123.1 |
. . 3
⊢ (𝜂 ↔ ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
3 | 2 | sbcbii 3755 |
. 2
⊢
([𝑗 / 𝑖]𝜂 ↔ [𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵)) |
4 | | bnj1123.3 |
. . . . . . . 8
⊢ 𝐾 = {𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
5 | | nfcv 2904 |
. . . . . . . . . 10
⊢
Ⅎ𝑖𝐷 |
6 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖 𝑓 Fn 𝑛 |
7 | | nfv 1922 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜑 |
8 | | bnj1123.4 |
. . . . . . . . . . . . 13
⊢ (𝜓 ↔ ∀𝑖 ∈ ω (suc 𝑖 ∈ 𝑛 → (𝑓‘suc 𝑖) = ∪ 𝑦 ∈ (𝑓‘𝑖) pred(𝑦, 𝐴, 𝑅))) |
9 | 8 | bnj1095 32474 |
. . . . . . . . . . . 12
⊢ (𝜓 → ∀𝑖𝜓) |
10 | 9 | nf5i 2146 |
. . . . . . . . . . 11
⊢
Ⅎ𝑖𝜓 |
11 | 6, 7, 10 | nf3an 1909 |
. . . . . . . . . 10
⊢
Ⅎ𝑖(𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) |
12 | 5, 11 | nfrex 3228 |
. . . . . . . . 9
⊢
Ⅎ𝑖∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓) |
13 | 12 | nfab 2910 |
. . . . . . . 8
⊢
Ⅎ𝑖{𝑓 ∣ ∃𝑛 ∈ 𝐷 (𝑓 Fn 𝑛 ∧ 𝜑 ∧ 𝜓)} |
14 | 4, 13 | nfcxfr 2902 |
. . . . . . 7
⊢
Ⅎ𝑖𝐾 |
15 | 14 | nfcri 2891 |
. . . . . 6
⊢
Ⅎ𝑖 𝑓 ∈ 𝐾 |
16 | | nfv 1922 |
. . . . . 6
⊢
Ⅎ𝑖 𝑗 ∈ dom 𝑓 |
17 | 15, 16 | nfan 1907 |
. . . . 5
⊢
Ⅎ𝑖(𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) |
18 | | nfv 1922 |
. . . . 5
⊢
Ⅎ𝑖(𝑓‘𝑗) ⊆ 𝐵 |
19 | 17, 18 | nfim 1904 |
. . . 4
⊢
Ⅎ𝑖((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵) |
20 | | eleq1w 2820 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑖 ∈ dom 𝑓 ↔ 𝑗 ∈ dom 𝑓)) |
21 | 20 | anbi2d 632 |
. . . . 5
⊢ (𝑖 = 𝑗 → ((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) ↔ (𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓))) |
22 | | fveq2 6717 |
. . . . . 6
⊢ (𝑖 = 𝑗 → (𝑓‘𝑖) = (𝑓‘𝑗)) |
23 | 22 | sseq1d 3932 |
. . . . 5
⊢ (𝑖 = 𝑗 → ((𝑓‘𝑖) ⊆ 𝐵 ↔ (𝑓‘𝑗) ⊆ 𝐵)) |
24 | 21, 23 | imbi12d 348 |
. . . 4
⊢ (𝑖 = 𝑗 → (((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))) |
25 | 19, 24 | sbciegf 3733 |
. . 3
⊢ (𝑗 ∈ V → ([𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵))) |
26 | 25 | elv 3414 |
. 2
⊢
([𝑗 / 𝑖]((𝑓 ∈ 𝐾 ∧ 𝑖 ∈ dom 𝑓) → (𝑓‘𝑖) ⊆ 𝐵) ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |
27 | 1, 3, 26 | 3bitri 300 |
1
⊢ (𝜂′ ↔ ((𝑓 ∈ 𝐾 ∧ 𝑗 ∈ dom 𝑓) → (𝑓‘𝑗) ⊆ 𝐵)) |