Proof of Theorem csbima12gALTVD
Step | Hyp | Ref
| Expression |
1 | | idn1 38790 |
. . . . . . 7
⊢ ( 𝐴 ∈ 𝐶 ▶ 𝐴 ∈ 𝐶 ) |
2 | | csbresgOLD 39055 |
. . . . . . 7
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)) |
3 | 1, 2 | e1a 38852 |
. . . . . 6
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) ) |
4 | | rneq 5351 |
. . . . . 6
⊢
(⦋𝐴 /
𝑥⦌(𝐹 ↾ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵)) |
5 | 3, 4 | e1a 38852 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐶 ▶ ran
⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) ) |
6 | | csbrngOLD 39056 |
. . . . . 6
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵)) |
7 | 1, 6 | e1a 38852 |
. . . . 5
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) ) |
8 | | eqeq2 2633 |
. . . . . 6
⊢ (ran
⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) ↔ ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))) |
9 | 8 | biimpd 219 |
. . . . 5
⊢ (ran
⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran ⦋𝐴 / 𝑥⦌(𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))) |
10 | 5, 7, 9 | e11 38913 |
. . . 4
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) ) |
11 | | df-ima 5127 |
. . . . . 6
⊢ (𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) |
12 | 11 | ax-gen 1722 |
. . . . 5
⊢
∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) |
13 | | csbeq2gOLD 38765 |
. . . . 5
⊢ (𝐴 ∈ 𝐶 → (∀𝑥(𝐹 “ 𝐵) = ran (𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵))) |
14 | 1, 12, 13 | e10 38919 |
. . . 4
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) ) |
15 | | eqeq2 2633 |
. . . . 5
⊢
(⦋𝐴 /
𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))) |
16 | 15 | biimpd 219 |
. . . 4
⊢
(⦋𝐴 /
𝑥⦌ran (𝐹 ↾ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ⦋𝐴 / 𝑥⦌ran (𝐹 ↾ 𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))) |
17 | 10, 14, 16 | e11 38913 |
. . 3
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) ) |
18 | | df-ima 5127 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) |
19 | | eqeq2 2633 |
. . . 4
⊢
((⦋𝐴 /
𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → (⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) ↔ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵))) |
20 | 19 | biimprcd 240 |
. . 3
⊢
(⦋𝐴 /
𝑥⦌(𝐹 “ 𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ((⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) = ran (⦋𝐴 / 𝑥⦌𝐹 ↾ ⦋𝐴 / 𝑥⦌𝐵) → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵))) |
21 | 17, 18, 20 | e10 38919 |
. 2
⊢ ( 𝐴 ∈ 𝐶 ▶ ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵) ) |
22 | 21 | in1 38787 |
1
⊢ (𝐴 ∈ 𝐶 → ⦋𝐴 / 𝑥⦌(𝐹 “ 𝐵) = (⦋𝐴 / 𝑥⦌𝐹 “ ⦋𝐴 / 𝑥⦌𝐵)) |