Proof of Theorem caseinj
Step | Hyp | Ref
| Expression |
1 | | df-inl 7020 |
. . . . . . 7
⊢ inl =
(𝑦 ∈ V ↦
〈∅, 𝑦〉) |
2 | 1 | funmpt2 5235 |
. . . . . 6
⊢ Fun
inl |
3 | | funcnvcnv 5255 |
. . . . . 6
⊢ (Fun inl
→ Fun ◡◡inl) |
4 | 2, 3 | ax-mp 5 |
. . . . 5
⊢ Fun ◡◡inl |
5 | | caseinj.r |
. . . . 5
⊢ (𝜑 → Fun ◡𝑅) |
6 | | funco 5236 |
. . . . 5
⊢ ((Fun
◡◡inl ∧ Fun ◡𝑅) → Fun (◡◡inl
∘ ◡𝑅)) |
7 | 4, 5, 6 | sylancr 412 |
. . . 4
⊢ (𝜑 → Fun (◡◡inl
∘ ◡𝑅)) |
8 | | cnvco 4794 |
. . . . 5
⊢ ◡(𝑅 ∘ ◡inl) = (◡◡inl
∘ ◡𝑅) |
9 | 8 | funeqi 5217 |
. . . 4
⊢ (Fun
◡(𝑅 ∘ ◡inl) ↔ Fun (◡◡inl
∘ ◡𝑅)) |
10 | 7, 9 | sylibr 133 |
. . 3
⊢ (𝜑 → Fun ◡(𝑅 ∘ ◡inl)) |
11 | | df-inr 7021 |
. . . . . . 7
⊢ inr =
(𝑥 ∈ V ↦
〈1o, 𝑥〉) |
12 | 11 | funmpt2 5235 |
. . . . . 6
⊢ Fun
inr |
13 | | funcnvcnv 5255 |
. . . . . 6
⊢ (Fun inr
→ Fun ◡◡inr) |
14 | 12, 13 | ax-mp 5 |
. . . . 5
⊢ Fun ◡◡inr |
15 | | caseinj.s |
. . . . 5
⊢ (𝜑 → Fun ◡𝑆) |
16 | | funco 5236 |
. . . . 5
⊢ ((Fun
◡◡inr ∧ Fun ◡𝑆) → Fun (◡◡inr
∘ ◡𝑆)) |
17 | 14, 15, 16 | sylancr 412 |
. . . 4
⊢ (𝜑 → Fun (◡◡inr
∘ ◡𝑆)) |
18 | | cnvco 4794 |
. . . . 5
⊢ ◡(𝑆 ∘ ◡inr) = (◡◡inr
∘ ◡𝑆) |
19 | 18 | funeqi 5217 |
. . . 4
⊢ (Fun
◡(𝑆 ∘ ◡inr) ↔ Fun (◡◡inr
∘ ◡𝑆)) |
20 | 17, 19 | sylibr 133 |
. . 3
⊢ (𝜑 → Fun ◡(𝑆 ∘ ◡inr)) |
21 | | df-rn 4620 |
. . . . . . 7
⊢ ran
(𝑅 ∘ ◡inl) = dom ◡(𝑅 ∘ ◡inl) |
22 | | rncoss 4879 |
. . . . . . 7
⊢ ran
(𝑅 ∘ ◡inl) ⊆ ran 𝑅 |
23 | 21, 22 | eqsstrri 3180 |
. . . . . 6
⊢ dom ◡(𝑅 ∘ ◡inl) ⊆ ran 𝑅 |
24 | | df-rn 4620 |
. . . . . . 7
⊢ ran
(𝑆 ∘ ◡inr) = dom ◡(𝑆 ∘ ◡inr) |
25 | | rncoss 4879 |
. . . . . . 7
⊢ ran
(𝑆 ∘ ◡inr) ⊆ ran 𝑆 |
26 | 24, 25 | eqsstrri 3180 |
. . . . . 6
⊢ dom ◡(𝑆 ∘ ◡inr) ⊆ ran 𝑆 |
27 | | ss2in 3355 |
. . . . . 6
⊢ ((dom
◡(𝑅 ∘ ◡inl) ⊆ ran 𝑅 ∧ dom ◡(𝑆 ∘ ◡inr) ⊆ ran 𝑆) → (dom ◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) ⊆ (ran 𝑅 ∩ ran 𝑆)) |
28 | 23, 26, 27 | mp2an 424 |
. . . . 5
⊢ (dom
◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) ⊆ (ran 𝑅 ∩ ran 𝑆) |
29 | | caseinj.disj |
. . . . 5
⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) |
30 | 28, 29 | sseqtrid 3197 |
. . . 4
⊢ (𝜑 → (dom ◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) ⊆ ∅) |
31 | | ss0 3454 |
. . . 4
⊢ ((dom
◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) ⊆ ∅ → (dom ◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) = ∅) |
32 | 30, 31 | syl 14 |
. . 3
⊢ (𝜑 → (dom ◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) = ∅) |
33 | | funun 5240 |
. . 3
⊢ (((Fun
◡(𝑅 ∘ ◡inl) ∧ Fun ◡(𝑆 ∘ ◡inr)) ∧ (dom ◡(𝑅 ∘ ◡inl) ∩ dom ◡(𝑆 ∘ ◡inr)) = ∅) → Fun (◡(𝑅 ∘ ◡inl) ∪ ◡(𝑆 ∘ ◡inr))) |
34 | 10, 20, 32, 33 | syl21anc 1232 |
. 2
⊢ (𝜑 → Fun (◡(𝑅 ∘ ◡inl) ∪ ◡(𝑆 ∘ ◡inr))) |
35 | | df-case 7057 |
. . . . 5
⊢
case(𝑅, 𝑆) = ((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) |
36 | 35 | cnveqi 4784 |
. . . 4
⊢ ◡case(𝑅, 𝑆) = ◡((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) |
37 | | cnvun 5014 |
. . . 4
⊢ ◡((𝑅 ∘ ◡inl) ∪ (𝑆 ∘ ◡inr)) = (◡(𝑅 ∘ ◡inl) ∪ ◡(𝑆 ∘ ◡inr)) |
38 | 36, 37 | eqtri 2191 |
. . 3
⊢ ◡case(𝑅, 𝑆) = (◡(𝑅 ∘ ◡inl) ∪ ◡(𝑆 ∘ ◡inr)) |
39 | 38 | funeqi 5217 |
. 2
⊢ (Fun
◡case(𝑅, 𝑆) ↔ Fun (◡(𝑅 ∘ ◡inl) ∪ ◡(𝑆 ∘ ◡inr))) |
40 | 34, 39 | sylibr 133 |
1
⊢ (𝜑 → Fun ◡case(𝑅, 𝑆)) |