Proof of Theorem casefun
Step | Hyp | Ref
| Expression |
1 | | casefun.f |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
2 | | djulf1o 7035 |
. . . . . 6
⊢
inl:V–1-1-onto→({∅} × V) |
3 | | f1of1 5441 |
. . . . . 6
⊢
(inl:V–1-1-onto→({∅} × V) → inl:V–1-1→({∅} × V)) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢
inl:V–1-1→({∅}
× V) |
5 | | df-f1 5203 |
. . . . . 6
⊢
(inl:V–1-1→({∅}
× V) ↔ (inl:V⟶({∅} × V) ∧ Fun ◡inl)) |
6 | 5 | simprbi 273 |
. . . . 5
⊢
(inl:V–1-1→({∅}
× V) → Fun ◡inl) |
7 | 4, 6 | mp1i 10 |
. . . 4
⊢ (𝜑 → Fun ◡inl) |
8 | | funco 5238 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun ◡inl) → Fun (𝐹 ∘ ◡inl)) |
9 | 1, 7, 8 | syl2anc 409 |
. . 3
⊢ (𝜑 → Fun (𝐹 ∘ ◡inl)) |
10 | | casefun.g |
. . . 4
⊢ (𝜑 → Fun 𝐺) |
11 | | djurf1o 7036 |
. . . . . 6
⊢
inr:V–1-1-onto→({1o} × V) |
12 | | f1of1 5441 |
. . . . . 6
⊢
(inr:V–1-1-onto→({1o} × V) →
inr:V–1-1→({1o}
× V)) |
13 | 11, 12 | ax-mp 5 |
. . . . 5
⊢
inr:V–1-1→({1o} × V) |
14 | | df-f1 5203 |
. . . . . 6
⊢
(inr:V–1-1→({1o} × V) ↔
(inr:V⟶({1o} × V) ∧ Fun ◡inr)) |
15 | 14 | simprbi 273 |
. . . . 5
⊢
(inr:V–1-1→({1o} × V) → Fun ◡inr) |
16 | 13, 15 | mp1i 10 |
. . . 4
⊢ (𝜑 → Fun ◡inr) |
17 | | funco 5238 |
. . . 4
⊢ ((Fun
𝐺 ∧ Fun ◡inr) → Fun (𝐺 ∘ ◡inr)) |
18 | 10, 16, 17 | syl2anc 409 |
. . 3
⊢ (𝜑 → Fun (𝐺 ∘ ◡inr)) |
19 | | dmcoss 4880 |
. . . . . . 7
⊢ dom
(𝐹 ∘ ◡inl) ⊆ dom ◡inl |
20 | | df-rn 4622 |
. . . . . . 7
⊢ ran inl =
dom ◡inl |
21 | 19, 20 | sseqtrri 3182 |
. . . . . 6
⊢ dom
(𝐹 ∘ ◡inl) ⊆ ran inl |
22 | | dmcoss 4880 |
. . . . . . 7
⊢ dom
(𝐺 ∘ ◡inr) ⊆ dom ◡inr |
23 | | df-rn 4622 |
. . . . . . 7
⊢ ran inr =
dom ◡inr |
24 | 22, 23 | sseqtrri 3182 |
. . . . . 6
⊢ dom
(𝐺 ∘ ◡inr) ⊆ ran inr |
25 | | ss2in 3355 |
. . . . . 6
⊢ ((dom
(𝐹 ∘ ◡inl) ⊆ ran inl ∧ dom (𝐺 ∘ ◡inr) ⊆ ran inr) → (dom (𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) ⊆ (ran inl ∩ ran
inr)) |
26 | 21, 24, 25 | mp2an 424 |
. . . . 5
⊢ (dom
(𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) ⊆ (ran inl ∩ ran
inr) |
27 | | rnresv 5070 |
. . . . . . . . 9
⊢ ran (inl
↾ V) = ran inl |
28 | 27 | eqcomi 2174 |
. . . . . . . 8
⊢ ran inl =
ran (inl ↾ V) |
29 | | rnresv 5070 |
. . . . . . . . 9
⊢ ran (inr
↾ V) = ran inr |
30 | 29 | eqcomi 2174 |
. . . . . . . 8
⊢ ran inr =
ran (inr ↾ V) |
31 | 28, 30 | ineq12i 3326 |
. . . . . . 7
⊢ (ran inl
∩ ran inr) = (ran (inl ↾ V) ∩ ran (inr ↾
V)) |
32 | | djuinr 7040 |
. . . . . . 7
⊢ (ran (inl
↾ V) ∩ ran (inr ↾ V)) = ∅ |
33 | 31, 32 | eqtri 2191 |
. . . . . 6
⊢ (ran inl
∩ ran inr) = ∅ |
34 | 33 | a1i 9 |
. . . . 5
⊢ (𝜑 → (ran inl ∩ ran inr) =
∅) |
35 | 26, 34 | sseqtrid 3197 |
. . . 4
⊢ (𝜑 → (dom (𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) ⊆ ∅) |
36 | | ss0 3455 |
. . . 4
⊢ ((dom
(𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) ⊆ ∅ → (dom (𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) = ∅) |
37 | 35, 36 | syl 14 |
. . 3
⊢ (𝜑 → (dom (𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) = ∅) |
38 | | funun 5242 |
. . 3
⊢ (((Fun
(𝐹 ∘ ◡inl) ∧ Fun (𝐺 ∘ ◡inr)) ∧ (dom (𝐹 ∘ ◡inl) ∩ dom (𝐺 ∘ ◡inr)) = ∅) → Fun ((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))) |
39 | 9, 18, 37, 38 | syl21anc 1232 |
. 2
⊢ (𝜑 → Fun ((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))) |
40 | | df-case 7061 |
. . 3
⊢
case(𝐹, 𝐺) = ((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr)) |
41 | 40 | funeqi 5219 |
. 2
⊢ (Fun
case(𝐹, 𝐺) ↔ Fun ((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))) |
42 | 39, 41 | sylibr 133 |
1
⊢ (𝜑 → Fun case(𝐹, 𝐺)) |