Proof of Theorem funimaeq
Step | Hyp | Ref
| Expression |
1 | | funimaeq.x |
. . . 4
⊢
Ⅎ𝑥𝜑 |
2 | | funimaeq.e |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) = (𝐺‘𝑥)) |
3 | | funimaeq.g |
. . . . . . . 8
⊢ (𝜑 → Fun 𝐺) |
4 | 3 | funfnd 6153 |
. . . . . . 7
⊢ (𝜑 → 𝐺 Fn dom 𝐺) |
5 | 4 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐺 Fn dom 𝐺) |
6 | | funimaeq.d |
. . . . . . 7
⊢ (𝜑 → 𝐴 ⊆ dom 𝐺) |
7 | 6 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ dom 𝐺) |
8 | | simpr 479 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝑥 ∈ 𝐴) |
9 | | fnfvima 6751 |
. . . . . 6
⊢ ((𝐺 Fn dom 𝐺 ∧ 𝐴 ⊆ dom 𝐺 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐴)) |
10 | 5, 7, 8, 9 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (𝐺 “ 𝐴)) |
11 | 2, 10 | eqeltrd 2905 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐺 “ 𝐴)) |
12 | 1, 11 | ralrimia 40128 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐺 “ 𝐴)) |
13 | | funimaeq.f |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
14 | | funimaeq.a |
. . . 4
⊢ (𝜑 → 𝐴 ⊆ dom 𝐹) |
15 | | funimass4 6493 |
. . . 4
⊢ ((Fun
𝐹 ∧ 𝐴 ⊆ dom 𝐹) → ((𝐹 “ 𝐴) ⊆ (𝐺 “ 𝐴) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐺 “ 𝐴))) |
16 | 13, 14, 15 | syl2anc 581 |
. . 3
⊢ (𝜑 → ((𝐹 “ 𝐴) ⊆ (𝐺 “ 𝐴) ↔ ∀𝑥 ∈ 𝐴 (𝐹‘𝑥) ∈ (𝐺 “ 𝐴))) |
17 | 12, 16 | mpbird 249 |
. 2
⊢ (𝜑 → (𝐹 “ 𝐴) ⊆ (𝐺 “ 𝐴)) |
18 | 2 | eqcomd 2830 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) = (𝐹‘𝑥)) |
19 | 13 | funfnd 6153 |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn dom 𝐹) |
20 | 19 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐹 Fn dom 𝐹) |
21 | 14 | adantr 474 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → 𝐴 ⊆ dom 𝐹) |
22 | | fnfvima 6751 |
. . . . . 6
⊢ ((𝐹 Fn dom 𝐹 ∧ 𝐴 ⊆ dom 𝐹 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐹 “ 𝐴)) |
23 | 20, 21, 8, 22 | syl3anc 1496 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐹‘𝑥) ∈ (𝐹 “ 𝐴)) |
24 | 18, 23 | eqeltrd 2905 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ 𝐴) → (𝐺‘𝑥) ∈ (𝐹 “ 𝐴)) |
25 | 1, 24 | ralrimia 40128 |
. . 3
⊢ (𝜑 → ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹 “ 𝐴)) |
26 | | funimass4 6493 |
. . . 4
⊢ ((Fun
𝐺 ∧ 𝐴 ⊆ dom 𝐺) → ((𝐺 “ 𝐴) ⊆ (𝐹 “ 𝐴) ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹 “ 𝐴))) |
27 | 3, 6, 26 | syl2anc 581 |
. . 3
⊢ (𝜑 → ((𝐺 “ 𝐴) ⊆ (𝐹 “ 𝐴) ↔ ∀𝑥 ∈ 𝐴 (𝐺‘𝑥) ∈ (𝐹 “ 𝐴))) |
28 | 25, 27 | mpbird 249 |
. 2
⊢ (𝜑 → (𝐺 “ 𝐴) ⊆ (𝐹 “ 𝐴)) |
29 | 17, 28 | eqssd 3843 |
1
⊢ (𝜑 → (𝐹 “ 𝐴) = (𝐺 “ 𝐴)) |