Proof of Theorem bnj1385
| Step | Hyp | Ref
| Expression |
| 1 | | nfv 1914 |
. . . . . . 7
⊢
Ⅎℎ(𝑓 ∈ 𝐴 → Fun 𝑓) |
| 2 | | bnj1385.4 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝐴 → ∀𝑓 𝑥 ∈ 𝐴) |
| 3 | 2 | nfcii 2894 |
. . . . . . . . 9
⊢
Ⅎ𝑓𝐴 |
| 4 | 3 | nfcri 2897 |
. . . . . . . 8
⊢
Ⅎ𝑓 ℎ ∈ 𝐴 |
| 5 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑓Fun ℎ |
| 6 | 4, 5 | nfim 1896 |
. . . . . . 7
⊢
Ⅎ𝑓(ℎ ∈ 𝐴 → Fun ℎ) |
| 7 | | eleq1w 2824 |
. . . . . . . 8
⊢ (𝑓 = ℎ → (𝑓 ∈ 𝐴 ↔ ℎ ∈ 𝐴)) |
| 8 | | funeq 6586 |
. . . . . . . 8
⊢ (𝑓 = ℎ → (Fun 𝑓 ↔ Fun ℎ)) |
| 9 | 7, 8 | imbi12d 344 |
. . . . . . 7
⊢ (𝑓 = ℎ → ((𝑓 ∈ 𝐴 → Fun 𝑓) ↔ (ℎ ∈ 𝐴 → Fun ℎ))) |
| 10 | 1, 6, 9 | cbvalv1 2343 |
. . . . . 6
⊢
(∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓) ↔ ∀ℎ(ℎ ∈ 𝐴 → Fun ℎ)) |
| 11 | | df-ral 3062 |
. . . . . 6
⊢
(∀𝑓 ∈
𝐴 Fun 𝑓 ↔ ∀𝑓(𝑓 ∈ 𝐴 → Fun 𝑓)) |
| 12 | | df-ral 3062 |
. . . . . 6
⊢
(∀ℎ ∈
𝐴 Fun ℎ ↔ ∀ℎ(ℎ ∈ 𝐴 → Fun ℎ)) |
| 13 | 10, 11, 12 | 3bitr4i 303 |
. . . . 5
⊢
(∀𝑓 ∈
𝐴 Fun 𝑓 ↔ ∀ℎ ∈ 𝐴 Fun ℎ) |
| 14 | | bnj1385.1 |
. . . . 5
⊢ (𝜑 ↔ ∀𝑓 ∈ 𝐴 Fun 𝑓) |
| 15 | | bnj1385.5 |
. . . . 5
⊢ (𝜑′ ↔ ∀ℎ ∈ 𝐴 Fun ℎ) |
| 16 | 13, 14, 15 | 3bitr4i 303 |
. . . 4
⊢ (𝜑 ↔ 𝜑′) |
| 17 | | nfv 1914 |
. . . . . 6
⊢
Ⅎℎ(𝑓 ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) |
| 18 | | nfv 1914 |
. . . . . . . 8
⊢
Ⅎ𝑓(ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸) |
| 19 | 3, 18 | nfralw 3311 |
. . . . . . 7
⊢
Ⅎ𝑓∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸) |
| 20 | 4, 19 | nfim 1896 |
. . . . . 6
⊢
Ⅎ𝑓(ℎ ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸)) |
| 21 | | dmeq 5914 |
. . . . . . . . . . . . 13
⊢ (𝑓 = ℎ → dom 𝑓 = dom ℎ) |
| 22 | 21 | ineq1d 4219 |
. . . . . . . . . . . 12
⊢ (𝑓 = ℎ → (dom 𝑓 ∩ dom 𝑔) = (dom ℎ ∩ dom 𝑔)) |
| 23 | | bnj1385.2 |
. . . . . . . . . . . 12
⊢ 𝐷 = (dom 𝑓 ∩ dom 𝑔) |
| 24 | | bnj1385.6 |
. . . . . . . . . . . 12
⊢ 𝐸 = (dom ℎ ∩ dom 𝑔) |
| 25 | 22, 23, 24 | 3eqtr4g 2802 |
. . . . . . . . . . 11
⊢ (𝑓 = ℎ → 𝐷 = 𝐸) |
| 26 | 25 | reseq2d 5997 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → (𝑓 ↾ 𝐷) = (𝑓 ↾ 𝐸)) |
| 27 | | reseq1 5991 |
. . . . . . . . . 10
⊢ (𝑓 = ℎ → (𝑓 ↾ 𝐸) = (ℎ ↾ 𝐸)) |
| 28 | 26, 27 | eqtrd 2777 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑓 ↾ 𝐷) = (ℎ ↾ 𝐸)) |
| 29 | 25 | reseq2d 5997 |
. . . . . . . . 9
⊢ (𝑓 = ℎ → (𝑔 ↾ 𝐷) = (𝑔 ↾ 𝐸)) |
| 30 | 28, 29 | eqeq12d 2753 |
. . . . . . . 8
⊢ (𝑓 = ℎ → ((𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) ↔ (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 31 | 30 | ralbidv 3178 |
. . . . . . 7
⊢ (𝑓 = ℎ → (∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) ↔ ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 32 | 7, 31 | imbi12d 344 |
. . . . . 6
⊢ (𝑓 = ℎ → ((𝑓 ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) ↔ (ℎ ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸)))) |
| 33 | 17, 20, 32 | cbvalv1 2343 |
. . . . 5
⊢
(∀𝑓(𝑓 ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) ↔ ∀ℎ(ℎ ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 34 | | df-ral 3062 |
. . . . 5
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) ↔ ∀𝑓(𝑓 ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) |
| 35 | | df-ral 3062 |
. . . . 5
⊢
(∀ℎ ∈
𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸) ↔ ∀ℎ(ℎ ∈ 𝐴 → ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 36 | 33, 34, 35 | 3bitr4i 303 |
. . . 4
⊢
(∀𝑓 ∈
𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷) ↔ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸)) |
| 37 | 16, 36 | anbi12i 628 |
. . 3
⊢ ((𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷)) ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 38 | | bnj1385.3 |
. . 3
⊢ (𝜓 ↔ (𝜑 ∧ ∀𝑓 ∈ 𝐴 ∀𝑔 ∈ 𝐴 (𝑓 ↾ 𝐷) = (𝑔 ↾ 𝐷))) |
| 39 | | bnj1385.7 |
. . 3
⊢ (𝜓′ ↔ (𝜑′ ∧ ∀ℎ ∈ 𝐴 ∀𝑔 ∈ 𝐴 (ℎ ↾ 𝐸) = (𝑔 ↾ 𝐸))) |
| 40 | 37, 38, 39 | 3bitr4i 303 |
. 2
⊢ (𝜓 ↔ 𝜓′) |
| 41 | 15, 24, 39 | bnj1383 34845 |
. 2
⊢ (𝜓′ → Fun ∪ 𝐴) |
| 42 | 40, 41 | sylbi 217 |
1
⊢ (𝜓 → Fun ∪ 𝐴) |