Step | Hyp | Ref
| Expression |
1 | | updjud.f |
. . . . 5
⊢ (𝜑 → 𝐹:𝐴⟶𝐶) |
2 | | updjud.g |
. . . . 5
⊢ (𝜑 → 𝐺:𝐵⟶𝐶) |
3 | | updjudhf.h |
. . . . 5
⊢ 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥)))) |
4 | 1, 2, 3 | updjudhf 9043 |
. . . 4
⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) |
5 | 4 | ffnd 6257 |
. . 3
⊢ (𝜑 → 𝐻 Fn (𝐴 ⊔ 𝐵)) |
6 | | inlresf 9026 |
. . . 4
⊢ (inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) |
7 | | ffn 6256 |
. . . 4
⊢ ((inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → (inl ↾ 𝐴) Fn 𝐴) |
8 | 6, 7 | mp1i 13 |
. . 3
⊢ (𝜑 → (inl ↾ 𝐴) Fn 𝐴) |
9 | | frn 6262 |
. . . 4
⊢ ((inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) |
10 | 6, 9 | mp1i 13 |
. . 3
⊢ (𝜑 → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) |
11 | | fnco 6210 |
. . 3
⊢ ((𝐻 Fn (𝐴 ⊔ 𝐵) ∧ (inl ↾ 𝐴) Fn 𝐴 ∧ ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴) |
12 | 5, 8, 10, 11 | syl3anc 1491 |
. 2
⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴) |
13 | 1 | ffnd 6257 |
. 2
⊢ (𝜑 → 𝐹 Fn 𝐴) |
14 | | fvco2 6498 |
. . . 4
⊢ (((inl
↾ 𝐴) Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎))) |
15 | 8, 14 | sylan 576 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎))) |
16 | | fvres 6430 |
. . . . . 6
⊢ (𝑎 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎)) |
17 | 16 | adantl 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎)) |
18 | 17 | fveq2d 6415 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐻‘(inl‘𝑎))) |
19 | 3 | a1i 11 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))) |
20 | | fveqeq2 6420 |
. . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → ((1st ‘𝑥) = ∅ ↔
(1st ‘(inl‘𝑎)) = ∅)) |
21 | | 2fveq3 6416 |
. . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → (𝐹‘(2nd ‘𝑥)) = (𝐹‘(2nd
‘(inl‘𝑎)))) |
22 | | 2fveq3 6416 |
. . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → (𝐺‘(2nd ‘𝑥)) = (𝐺‘(2nd
‘(inl‘𝑎)))) |
23 | 20, 21, 22 | ifbieq12d 4304 |
. . . . . . 7
⊢ (𝑥 = (inl‘𝑎) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎))))) |
24 | 23 | adantl 474 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎))))) |
25 | | 1stinl 9039 |
. . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → (1st
‘(inl‘𝑎)) =
∅) |
26 | 25 | adantl 474 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1st
‘(inl‘𝑎)) =
∅) |
27 | 26 | adantr 473 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → (1st
‘(inl‘𝑎)) =
∅) |
28 | 27 | iftrued 4285 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎)))) =
(𝐹‘(2nd
‘(inl‘𝑎)))) |
29 | 24, 28 | eqtrd 2833 |
. . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = (𝐹‘(2nd
‘(inl‘𝑎)))) |
30 | | djulcl 9022 |
. . . . . 6
⊢ (𝑎 ∈ 𝐴 → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵)) |
31 | 30 | adantl 474 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵)) |
32 | 1 | adantr 473 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐹:𝐴⟶𝐶) |
33 | | 2ndinl 9040 |
. . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → (2nd
‘(inl‘𝑎)) =
𝑎) |
34 | 33 | adantl 474 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd
‘(inl‘𝑎)) =
𝑎) |
35 | | simpr 478 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) |
36 | 34, 35 | eqeltrd 2878 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd
‘(inl‘𝑎))
∈ 𝐴) |
37 | 32, 36 | ffvelrnd 6586 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd
‘(inl‘𝑎)))
∈ 𝐶) |
38 | 19, 29, 31, 37 | fvmptd 6513 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘(inl‘𝑎)) = (𝐹‘(2nd
‘(inl‘𝑎)))) |
39 | 18, 38 | eqtrd 2833 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐹‘(2nd
‘(inl‘𝑎)))) |
40 | 34 | fveq2d 6415 |
. . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd
‘(inl‘𝑎))) =
(𝐹‘𝑎)) |
41 | 15, 39, 40 | 3eqtrd 2837 |
. 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐹‘𝑎)) |
42 | 12, 13, 41 | eqfnfvd 6540 |
1
⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹) |