Proof of Theorem afvco2
Step | Hyp | Ref
| Expression |
1 | | fvco2 6273 |
. . . . 5
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
2 | 1 | adantl 482 |
. . . 4
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘ 𝐺)‘𝑋) = (𝐹‘(𝐺‘𝑋))) |
3 | | simpll 790 |
. . . . . 6
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝐺‘𝑋) ∈ dom 𝐹) |
4 | | df-fn 5891 |
. . . . . . . . 9
⊢ (𝐺 Fn 𝐴 ↔ (Fun 𝐺 ∧ dom 𝐺 = 𝐴)) |
5 | | simpll 790 |
. . . . . . . . . 10
⊢ (((Fun
𝐺 ∧ dom 𝐺 = 𝐴) ∧ 𝑋 ∈ 𝐴) → Fun 𝐺) |
6 | | eleq2 2690 |
. . . . . . . . . . . . . 14
⊢ (𝐴 = dom 𝐺 → (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ dom 𝐺)) |
7 | 6 | eqcoms 2630 |
. . . . . . . . . . . . 13
⊢ (dom
𝐺 = 𝐴 → (𝑋 ∈ 𝐴 ↔ 𝑋 ∈ dom 𝐺)) |
8 | 7 | biimpd 219 |
. . . . . . . . . . . 12
⊢ (dom
𝐺 = 𝐴 → (𝑋 ∈ 𝐴 → 𝑋 ∈ dom 𝐺)) |
9 | 8 | adantl 482 |
. . . . . . . . . . 11
⊢ ((Fun
𝐺 ∧ dom 𝐺 = 𝐴) → (𝑋 ∈ 𝐴 → 𝑋 ∈ dom 𝐺)) |
10 | 9 | imp 445 |
. . . . . . . . . 10
⊢ (((Fun
𝐺 ∧ dom 𝐺 = 𝐴) ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺) |
11 | 5, 10 | jca 554 |
. . . . . . . . 9
⊢ (((Fun
𝐺 ∧ dom 𝐺 = 𝐴) ∧ 𝑋 ∈ 𝐴) → (Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺)) |
12 | 4, 11 | sylanb 489 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺)) |
13 | 12 | adantl 482 |
. . . . . . 7
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (Fun 𝐺 ∧ 𝑋 ∈ dom 𝐺)) |
14 | | dmfco 6272 |
. . . . . . 7
⊢ ((Fun
𝐺 ∧ 𝑋 ∈ dom 𝐺) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹)) |
15 | 13, 14 | syl 17 |
. . . . . 6
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹)) |
16 | 3, 15 | mpbird 247 |
. . . . 5
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → 𝑋 ∈ dom (𝐹 ∘ 𝐺)) |
17 | | funcoressn 41207 |
. . . . 5
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) |
18 | | df-dfat 41196 |
. . . . . 6
⊢ ((𝐹 ∘ 𝐺) defAt 𝑋 ↔ (𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋}))) |
19 | | afvfundmfveq 41218 |
. . . . . 6
⊢ ((𝐹 ∘ 𝐺) defAt 𝑋 → ((𝐹 ∘ 𝐺)'''𝑋) = ((𝐹 ∘ 𝐺)‘𝑋)) |
20 | 18, 19 | sylbir 225 |
. . . . 5
⊢ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) → ((𝐹 ∘ 𝐺)'''𝑋) = ((𝐹 ∘ 𝐺)‘𝑋)) |
21 | 16, 17, 20 | syl2anc 693 |
. . . 4
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘ 𝐺)'''𝑋) = ((𝐹 ∘ 𝐺)‘𝑋)) |
22 | | df-dfat 41196 |
. . . . . 6
⊢ (𝐹 defAt (𝐺‘𝑋) ↔ ((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)}))) |
23 | | afvfundmfveq 41218 |
. . . . . 6
⊢ (𝐹 defAt (𝐺‘𝑋) → (𝐹'''(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))) |
24 | 22, 23 | sylbir 225 |
. . . . 5
⊢ (((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) → (𝐹'''(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))) |
25 | 24 | adantr 481 |
. . . 4
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → (𝐹'''(𝐺‘𝑋)) = (𝐹‘(𝐺‘𝑋))) |
26 | 2, 21, 25 | 3eqtr4d 2666 |
. . 3
⊢ ((((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺‘𝑋))) |
27 | | ianor 509 |
. . . . . 6
⊢ (¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ↔ (¬ (𝐺‘𝑋) ∈ dom 𝐹 ∨ ¬ Fun (𝐹 ↾ {(𝐺‘𝑋)}))) |
28 | 14 | funfni 5991 |
. . . . . . . . . . 11
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝑋 ∈ dom (𝐹 ∘ 𝐺) ↔ (𝐺‘𝑋) ∈ dom 𝐹)) |
29 | 28 | bicomd 213 |
. . . . . . . . . 10
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐺‘𝑋) ∈ dom 𝐹 ↔ 𝑋 ∈ dom (𝐹 ∘ 𝐺))) |
30 | 29 | notbid 308 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (¬ (𝐺‘𝑋) ∈ dom 𝐹 ↔ ¬ 𝑋 ∈ dom (𝐹 ∘ 𝐺))) |
31 | 30 | biimpd 219 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (¬ (𝐺‘𝑋) ∈ dom 𝐹 → ¬ 𝑋 ∈ dom (𝐹 ∘ 𝐺))) |
32 | | ndmafv 41220 |
. . . . . . . 8
⊢ (¬
𝑋 ∈ dom (𝐹 ∘ 𝐺) → ((𝐹 ∘ 𝐺)'''𝑋) = V) |
33 | 31, 32 | syl6com 37 |
. . . . . . 7
⊢ (¬
(𝐺‘𝑋) ∈ dom 𝐹 → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = V)) |
34 | | funressnfv 41208 |
. . . . . . . . . . . 12
⊢ (((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → Fun (𝐹 ↾ {(𝐺‘𝑋)})) |
35 | 34 | ex 450 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))) |
36 | | afvnfundmuv 41219 |
. . . . . . . . . . . 12
⊢ (¬
(𝐹 ∘ 𝐺) defAt 𝑋 → ((𝐹 ∘ 𝐺)'''𝑋) = V) |
37 | 18, 36 | sylnbir 321 |
. . . . . . . . . . 11
⊢ (¬
(𝑋 ∈ dom (𝐹 ∘ 𝐺) ∧ Fun ((𝐹 ∘ 𝐺) ↾ {𝑋})) → ((𝐹 ∘ 𝐺)'''𝑋) = V) |
38 | 35, 37 | nsyl4 156 |
. . . . . . . . . 10
⊢ (¬
((𝐹 ∘ 𝐺)'''𝑋) = V → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → Fun (𝐹 ↾ {(𝐺‘𝑋)}))) |
39 | 38 | com12 32 |
. . . . . . . . 9
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (¬ ((𝐹 ∘ 𝐺)'''𝑋) = V → Fun (𝐹 ↾ {(𝐺‘𝑋)}))) |
40 | 39 | con1d 139 |
. . . . . . . 8
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (¬ Fun (𝐹 ↾ {(𝐺‘𝑋)}) → ((𝐹 ∘ 𝐺)'''𝑋) = V)) |
41 | 40 | com12 32 |
. . . . . . 7
⊢ (¬
Fun (𝐹 ↾ {(𝐺‘𝑋)}) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = V)) |
42 | 33, 41 | jaoi 394 |
. . . . . 6
⊢ ((¬
(𝐺‘𝑋) ∈ dom 𝐹 ∨ ¬ Fun (𝐹 ↾ {(𝐺‘𝑋)})) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = V)) |
43 | 27, 42 | sylbi 207 |
. . . . 5
⊢ (¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) → ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = V)) |
44 | 43 | imp 445 |
. . . 4
⊢ ((¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘ 𝐺)'''𝑋) = V) |
45 | | afvnfundmuv 41219 |
. . . . . . 7
⊢ (¬
𝐹 defAt (𝐺‘𝑋) → (𝐹'''(𝐺‘𝑋)) = V) |
46 | 22, 45 | sylnbir 321 |
. . . . . 6
⊢ (¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) → (𝐹'''(𝐺‘𝑋)) = V) |
47 | 46 | eqcomd 2628 |
. . . . 5
⊢ (¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) → V = (𝐹'''(𝐺‘𝑋))) |
48 | 47 | adantr 481 |
. . . 4
⊢ ((¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → V = (𝐹'''(𝐺‘𝑋))) |
49 | 44, 48 | eqtrd 2656 |
. . 3
⊢ ((¬
((𝐺‘𝑋) ∈ dom 𝐹 ∧ Fun (𝐹 ↾ {(𝐺‘𝑋)})) ∧ (𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴)) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺‘𝑋))) |
50 | 26, 49 | pm2.61ian 831 |
. 2
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺‘𝑋))) |
51 | | eqidd 2623 |
. . 3
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝐹 = 𝐹) |
52 | 4, 9 | sylbi 207 |
. . . . . 6
⊢ (𝐺 Fn 𝐴 → (𝑋 ∈ 𝐴 → 𝑋 ∈ dom 𝐺)) |
53 | 52 | imp 445 |
. . . . 5
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → 𝑋 ∈ dom 𝐺) |
54 | | fnfun 5988 |
. . . . . . 7
⊢ (𝐺 Fn 𝐴 → Fun 𝐺) |
55 | | funres 5929 |
. . . . . . 7
⊢ (Fun
𝐺 → Fun (𝐺 ↾ {𝑋})) |
56 | 54, 55 | syl 17 |
. . . . . 6
⊢ (𝐺 Fn 𝐴 → Fun (𝐺 ↾ {𝑋})) |
57 | 56 | adantr 481 |
. . . . 5
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → Fun (𝐺 ↾ {𝑋})) |
58 | | df-dfat 41196 |
. . . . . 6
⊢ (𝐺 defAt 𝑋 ↔ (𝑋 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝑋}))) |
59 | | afvfundmfveq 41218 |
. . . . . 6
⊢ (𝐺 defAt 𝑋 → (𝐺'''𝑋) = (𝐺‘𝑋)) |
60 | 58, 59 | sylbir 225 |
. . . . 5
⊢ ((𝑋 ∈ dom 𝐺 ∧ Fun (𝐺 ↾ {𝑋})) → (𝐺'''𝑋) = (𝐺‘𝑋)) |
61 | 53, 57, 60 | syl2anc 693 |
. . . 4
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐺'''𝑋) = (𝐺‘𝑋)) |
62 | 61 | eqcomd 2628 |
. . 3
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐺‘𝑋) = (𝐺'''𝑋)) |
63 | 51, 62 | afveq12d 41213 |
. 2
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → (𝐹'''(𝐺‘𝑋)) = (𝐹'''(𝐺'''𝑋))) |
64 | 50, 63 | eqtrd 2656 |
1
⊢ ((𝐺 Fn 𝐴 ∧ 𝑋 ∈ 𝐴) → ((𝐹 ∘ 𝐺)'''𝑋) = (𝐹'''(𝐺'''𝑋))) |