| 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 9971 | . . . 4
⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) | 
| 5 | 4 | ffnd 6737 | . . 3
⊢ (𝜑 → 𝐻 Fn (𝐴 ⊔ 𝐵)) | 
| 6 |  | inlresf 9954 | . . . 4
⊢ (inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) | 
| 7 |  | ffn 6736 | . . . 4
⊢ ((inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → (inl ↾ 𝐴) Fn 𝐴) | 
| 8 | 6, 7 | mp1i 13 | . . 3
⊢ (𝜑 → (inl ↾ 𝐴) Fn 𝐴) | 
| 9 |  | frn 6743 | . . . 4
⊢ ((inl
↾ 𝐴):𝐴⟶(𝐴 ⊔ 𝐵) → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) | 
| 10 | 6, 9 | mp1i 13 | . . 3
⊢ (𝜑 → ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) | 
| 11 |  | fnco 6686 | . . 3
⊢ ((𝐻 Fn (𝐴 ⊔ 𝐵) ∧ (inl ↾ 𝐴) Fn 𝐴 ∧ ran (inl ↾ 𝐴) ⊆ (𝐴 ⊔ 𝐵)) → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴) | 
| 12 | 5, 8, 10, 11 | syl3anc 1373 | . 2
⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) Fn 𝐴) | 
| 13 | 1 | ffnd 6737 | . 2
⊢ (𝜑 → 𝐹 Fn 𝐴) | 
| 14 |  | fvco2 7006 | . . . 4
⊢ (((inl
↾ 𝐴) Fn 𝐴 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎))) | 
| 15 | 8, 14 | sylan 580 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐻‘((inl ↾ 𝐴)‘𝑎))) | 
| 16 |  | fvres 6925 | . . . . . 6
⊢ (𝑎 ∈ 𝐴 → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎)) | 
| 17 | 16 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((inl ↾ 𝐴)‘𝑎) = (inl‘𝑎)) | 
| 18 | 17 | fveq2d 6910 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐻‘(inl‘𝑎))) | 
| 19 |  | fveqeq2 6915 | . . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → ((1st ‘𝑥) = ∅ ↔
(1st ‘(inl‘𝑎)) = ∅)) | 
| 20 |  | 2fveq3 6911 | . . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → (𝐹‘(2nd ‘𝑥)) = (𝐹‘(2nd
‘(inl‘𝑎)))) | 
| 21 |  | 2fveq3 6911 | . . . . . . . 8
⊢ (𝑥 = (inl‘𝑎) → (𝐺‘(2nd ‘𝑥)) = (𝐺‘(2nd
‘(inl‘𝑎)))) | 
| 22 | 19, 20, 21 | ifbieq12d 4554 | . . . . . . 7
⊢ (𝑥 = (inl‘𝑎) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎))))) | 
| 23 | 22 | adantl 481 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎))))) | 
| 24 |  | 1stinl 9967 | . . . . . . . . 9
⊢ (𝑎 ∈ 𝐴 → (1st
‘(inl‘𝑎)) =
∅) | 
| 25 | 24 | adantl 481 | . . . . . . . 8
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (1st
‘(inl‘𝑎)) =
∅) | 
| 26 | 25 | adantr 480 | . . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → (1st
‘(inl‘𝑎)) =
∅) | 
| 27 | 26 | iftrued 4533 | . . . . . 6
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st
‘(inl‘𝑎)) =
∅, (𝐹‘(2nd
‘(inl‘𝑎))),
(𝐺‘(2nd
‘(inl‘𝑎)))) =
(𝐹‘(2nd
‘(inl‘𝑎)))) | 
| 28 | 23, 27 | eqtrd 2777 | . . . . 5
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐴) ∧ 𝑥 = (inl‘𝑎)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = (𝐹‘(2nd
‘(inl‘𝑎)))) | 
| 29 |  | djulcl 9950 | . . . . . 6
⊢ (𝑎 ∈ 𝐴 → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵)) | 
| 30 | 29 | adantl 481 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (inl‘𝑎) ∈ (𝐴 ⊔ 𝐵)) | 
| 31 | 1 | adantr 480 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝐹:𝐴⟶𝐶) | 
| 32 |  | 2ndinl 9968 | . . . . . . . 8
⊢ (𝑎 ∈ 𝐴 → (2nd
‘(inl‘𝑎)) =
𝑎) | 
| 33 | 32 | adantl 481 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd
‘(inl‘𝑎)) =
𝑎) | 
| 34 |  | simpr 484 | . . . . . . 7
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → 𝑎 ∈ 𝐴) | 
| 35 | 33, 34 | eqeltrd 2841 | . . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (2nd
‘(inl‘𝑎))
∈ 𝐴) | 
| 36 | 31, 35 | ffvelcdmd 7105 | . . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd
‘(inl‘𝑎)))
∈ 𝐶) | 
| 37 | 3, 28, 30, 36 | fvmptd2 7024 | . . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘(inl‘𝑎)) = (𝐹‘(2nd
‘(inl‘𝑎)))) | 
| 38 | 18, 37 | eqtrd 2777 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐻‘((inl ↾ 𝐴)‘𝑎)) = (𝐹‘(2nd
‘(inl‘𝑎)))) | 
| 39 | 33 | fveq2d 6910 | . . 3
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → (𝐹‘(2nd
‘(inl‘𝑎))) =
(𝐹‘𝑎)) | 
| 40 | 15, 38, 39 | 3eqtrd 2781 | . 2
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐴) → ((𝐻 ∘ (inl ↾ 𝐴))‘𝑎) = (𝐹‘𝑎)) | 
| 41 | 12, 13, 40 | eqfnfvd 7054 | 1
⊢ (𝜑 → (𝐻 ∘ (inl ↾ 𝐴)) = 𝐹) |