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 7056 |
. . . 4
⊢ (𝜑 → 𝐻:(𝐴 ⊔ 𝐵)⟶𝐶) |
5 | | ffn 5347 |
. . . 4
⊢ (𝐻:(𝐴 ⊔ 𝐵)⟶𝐶 → 𝐻 Fn (𝐴 ⊔ 𝐵)) |
6 | 4, 5 | syl 14 |
. . 3
⊢ (𝜑 → 𝐻 Fn (𝐴 ⊔ 𝐵)) |
7 | | inrresf1 7039 |
. . . 4
⊢ (inr
↾ 𝐵):𝐵–1-1→(𝐴 ⊔ 𝐵) |
8 | | f1fn 5405 |
. . . 4
⊢ ((inr
↾ 𝐵):𝐵–1-1→(𝐴 ⊔ 𝐵) → (inr ↾ 𝐵) Fn 𝐵) |
9 | 7, 8 | mp1i 10 |
. . 3
⊢ (𝜑 → (inr ↾ 𝐵) Fn 𝐵) |
10 | | f1f 5403 |
. . . . 5
⊢ ((inr
↾ 𝐵):𝐵–1-1→(𝐴 ⊔ 𝐵) → (inr ↾ 𝐵):𝐵⟶(𝐴 ⊔ 𝐵)) |
11 | 7, 10 | ax-mp 5 |
. . . 4
⊢ (inr
↾ 𝐵):𝐵⟶(𝐴 ⊔ 𝐵) |
12 | | frn 5356 |
. . . 4
⊢ ((inr
↾ 𝐵):𝐵⟶(𝐴 ⊔ 𝐵) → ran (inr ↾ 𝐵) ⊆ (𝐴 ⊔ 𝐵)) |
13 | 11, 12 | mp1i 10 |
. . 3
⊢ (𝜑 → ran (inr ↾ 𝐵) ⊆ (𝐴 ⊔ 𝐵)) |
14 | | fnco 5306 |
. . 3
⊢ ((𝐻 Fn (𝐴 ⊔ 𝐵) ∧ (inr ↾ 𝐵) Fn 𝐵 ∧ ran (inr ↾ 𝐵) ⊆ (𝐴 ⊔ 𝐵)) → (𝐻 ∘ (inr ↾ 𝐵)) Fn 𝐵) |
15 | 6, 9, 13, 14 | syl3anc 1233 |
. 2
⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) Fn 𝐵) |
16 | | ffn 5347 |
. . 3
⊢ (𝐺:𝐵⟶𝐶 → 𝐺 Fn 𝐵) |
17 | 2, 16 | syl 14 |
. 2
⊢ (𝜑 → 𝐺 Fn 𝐵) |
18 | | fvco2 5565 |
. . . 4
⊢ (((inr
↾ 𝐵) Fn 𝐵 ∧ 𝑏 ∈ 𝐵) → ((𝐻 ∘ (inr ↾ 𝐵))‘𝑏) = (𝐻‘((inr ↾ 𝐵)‘𝑏))) |
19 | 9, 18 | sylan 281 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐻 ∘ (inr ↾ 𝐵))‘𝑏) = (𝐻‘((inr ↾ 𝐵)‘𝑏))) |
20 | | fvres 5520 |
. . . . . 6
⊢ (𝑏 ∈ 𝐵 → ((inr ↾ 𝐵)‘𝑏) = (inr‘𝑏)) |
21 | 20 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((inr ↾ 𝐵)‘𝑏) = (inr‘𝑏)) |
22 | 21 | fveq2d 5500 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐻‘((inr ↾ 𝐵)‘𝑏)) = (𝐻‘(inr‘𝑏))) |
23 | 3 | a1i 9 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐻 = (𝑥 ∈ (𝐴 ⊔ 𝐵) ↦ if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))))) |
24 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑥 = (inr‘𝑏) → (1st ‘𝑥) = (1st
‘(inr‘𝑏))) |
25 | 24 | eqeq1d 2179 |
. . . . . . . 8
⊢ (𝑥 = (inr‘𝑏) → ((1st ‘𝑥) = ∅ ↔
(1st ‘(inr‘𝑏)) = ∅)) |
26 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑥 = (inr‘𝑏) → (2nd ‘𝑥) = (2nd
‘(inr‘𝑏))) |
27 | 26 | fveq2d 5500 |
. . . . . . . 8
⊢ (𝑥 = (inr‘𝑏) → (𝐹‘(2nd ‘𝑥)) = (𝐹‘(2nd
‘(inr‘𝑏)))) |
28 | 26 | fveq2d 5500 |
. . . . . . . 8
⊢ (𝑥 = (inr‘𝑏) → (𝐺‘(2nd ‘𝑥)) = (𝐺‘(2nd
‘(inr‘𝑏)))) |
29 | 25, 27, 28 | ifbieq12d 3552 |
. . . . . . 7
⊢ (𝑥 = (inr‘𝑏) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inr‘𝑏)) =
∅, (𝐹‘(2nd
‘(inr‘𝑏))),
(𝐺‘(2nd
‘(inr‘𝑏))))) |
30 | 29 | adantl 275 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (inr‘𝑏)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = if((1st
‘(inr‘𝑏)) =
∅, (𝐹‘(2nd
‘(inr‘𝑏))),
(𝐺‘(2nd
‘(inr‘𝑏))))) |
31 | | 1stinr 7053 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐵 → (1st
‘(inr‘𝑏)) =
1o) |
32 | | 1n0 6411 |
. . . . . . . . . . . 12
⊢
1o ≠ ∅ |
33 | 32 | neii 2342 |
. . . . . . . . . . 11
⊢ ¬
1o = ∅ |
34 | | eqeq1 2177 |
. . . . . . . . . . 11
⊢
((1st ‘(inr‘𝑏)) = 1o → ((1st
‘(inr‘𝑏)) =
∅ ↔ 1o = ∅)) |
35 | 33, 34 | mtbiri 670 |
. . . . . . . . . 10
⊢
((1st ‘(inr‘𝑏)) = 1o → ¬
(1st ‘(inr‘𝑏)) = ∅) |
36 | 31, 35 | syl 14 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐵 → ¬ (1st
‘(inr‘𝑏)) =
∅) |
37 | 36 | adantl 275 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ¬ (1st
‘(inr‘𝑏)) =
∅) |
38 | 37 | adantr 274 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (inr‘𝑏)) → ¬ (1st
‘(inr‘𝑏)) =
∅) |
39 | 38 | iffalsed 3536 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (inr‘𝑏)) → if((1st
‘(inr‘𝑏)) =
∅, (𝐹‘(2nd
‘(inr‘𝑏))),
(𝐺‘(2nd
‘(inr‘𝑏)))) =
(𝐺‘(2nd
‘(inr‘𝑏)))) |
40 | 30, 39 | eqtrd 2203 |
. . . . 5
⊢ (((𝜑 ∧ 𝑏 ∈ 𝐵) ∧ 𝑥 = (inr‘𝑏)) → if((1st ‘𝑥) = ∅, (𝐹‘(2nd ‘𝑥)), (𝐺‘(2nd ‘𝑥))) = (𝐺‘(2nd
‘(inr‘𝑏)))) |
41 | | djurcl 7029 |
. . . . . 6
⊢ (𝑏 ∈ 𝐵 → (inr‘𝑏) ∈ (𝐴 ⊔ 𝐵)) |
42 | 41 | adantl 275 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (inr‘𝑏) ∈ (𝐴 ⊔ 𝐵)) |
43 | 2 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝐺:𝐵⟶𝐶) |
44 | | 2ndinr 7054 |
. . . . . . . 8
⊢ (𝑏 ∈ 𝐵 → (2nd
‘(inr‘𝑏)) =
𝑏) |
45 | 44 | adantl 275 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (2nd
‘(inr‘𝑏)) =
𝑏) |
46 | | simpr 109 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → 𝑏 ∈ 𝐵) |
47 | 45, 46 | eqeltrd 2247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (2nd
‘(inr‘𝑏))
∈ 𝐵) |
48 | 43, 47 | ffvelrnd 5632 |
. . . . 5
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐺‘(2nd
‘(inr‘𝑏)))
∈ 𝐶) |
49 | 23, 40, 42, 48 | fvmptd 5577 |
. . . 4
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐻‘(inr‘𝑏)) = (𝐺‘(2nd
‘(inr‘𝑏)))) |
50 | 22, 49 | eqtrd 2203 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐻‘((inr ↾ 𝐵)‘𝑏)) = (𝐺‘(2nd
‘(inr‘𝑏)))) |
51 | 45 | fveq2d 5500 |
. . 3
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → (𝐺‘(2nd
‘(inr‘𝑏))) =
(𝐺‘𝑏)) |
52 | 19, 50, 51 | 3eqtrd 2207 |
. 2
⊢ ((𝜑 ∧ 𝑏 ∈ 𝐵) → ((𝐻 ∘ (inr ↾ 𝐵))‘𝑏) = (𝐺‘𝑏)) |
53 | 15, 17, 52 | eqfnfvd 5596 |
1
⊢ (𝜑 → (𝐻 ∘ (inr ↾ 𝐵)) = 𝐺) |