Proof of Theorem djuinj
Step | Hyp | Ref
| Expression |
1 | | inlresf1 7038 |
. . . . . . 7
⊢ (inl
↾ dom 𝑅):dom 𝑅–1-1→(dom 𝑅 ⊔ 𝐴) |
2 | | f1fun 5406 |
. . . . . . 7
⊢ ((inl
↾ dom 𝑅):dom 𝑅–1-1→(dom 𝑅 ⊔ 𝐴) → Fun (inl ↾ dom 𝑅)) |
3 | 1, 2 | ax-mp 5 |
. . . . . 6
⊢ Fun (inl
↾ dom 𝑅) |
4 | | funcnvcnv 5257 |
. . . . . 6
⊢ (Fun (inl
↾ dom 𝑅) → Fun
◡◡(inl ↾ dom 𝑅)) |
5 | 3, 4 | ax-mp 5 |
. . . . 5
⊢ Fun ◡◡(inl ↾ dom 𝑅) |
6 | | djuinj.r |
. . . . 5
⊢ (𝜑 → Fun ◡𝑅) |
7 | | funco 5238 |
. . . . 5
⊢ ((Fun
◡◡(inl ↾ dom 𝑅) ∧ Fun ◡𝑅) → Fun (◡◡(inl ↾ dom 𝑅) ∘ ◡𝑅)) |
8 | 5, 6, 7 | sylancr 412 |
. . . 4
⊢ (𝜑 → Fun (◡◡(inl ↾ dom 𝑅) ∘ ◡𝑅)) |
9 | | cnvco 4796 |
. . . . 5
⊢ ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) = (◡◡(inl ↾ dom 𝑅) ∘ ◡𝑅) |
10 | 9 | funeqi 5219 |
. . . 4
⊢ (Fun
◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ↔ Fun (◡◡(inl ↾ dom 𝑅) ∘ ◡𝑅)) |
11 | 8, 10 | sylibr 133 |
. . 3
⊢ (𝜑 → Fun ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅))) |
12 | | inrresf1 7039 |
. . . . . . 7
⊢ (inr
↾ dom 𝑆):dom 𝑆–1-1→(𝐴 ⊔ dom 𝑆) |
13 | | f1fun 5406 |
. . . . . . 7
⊢ ((inr
↾ dom 𝑆):dom 𝑆–1-1→(𝐴 ⊔ dom 𝑆) → Fun (inr ↾ dom 𝑆)) |
14 | 12, 13 | ax-mp 5 |
. . . . . 6
⊢ Fun (inr
↾ dom 𝑆) |
15 | | funcnvcnv 5257 |
. . . . . 6
⊢ (Fun (inr
↾ dom 𝑆) → Fun
◡◡(inr ↾ dom 𝑆)) |
16 | 14, 15 | ax-mp 5 |
. . . . 5
⊢ Fun ◡◡(inr ↾ dom 𝑆) |
17 | | djuinj.s |
. . . . 5
⊢ (𝜑 → Fun ◡𝑆) |
18 | | funco 5238 |
. . . . 5
⊢ ((Fun
◡◡(inr ↾ dom 𝑆) ∧ Fun ◡𝑆) → Fun (◡◡(inr ↾ dom 𝑆) ∘ ◡𝑆)) |
19 | 16, 17, 18 | sylancr 412 |
. . . 4
⊢ (𝜑 → Fun (◡◡(inr ↾ dom 𝑆) ∘ ◡𝑆)) |
20 | | cnvco 4796 |
. . . . 5
⊢ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)) = (◡◡(inr ↾ dom 𝑆) ∘ ◡𝑆) |
21 | 20 | funeqi 5219 |
. . . 4
⊢ (Fun
◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)) ↔ Fun (◡◡(inr ↾ dom 𝑆) ∘ ◡𝑆)) |
22 | 19, 21 | sylibr 133 |
. . 3
⊢ (𝜑 → Fun ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
23 | | df-rn 4622 |
. . . . . . 7
⊢ ran
(𝑅 ∘ ◡(inl ↾ dom 𝑅)) = dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) |
24 | | rncoss 4881 |
. . . . . . 7
⊢ ran
(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ⊆ ran 𝑅 |
25 | 23, 24 | eqsstrri 3180 |
. . . . . 6
⊢ dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ⊆ ran 𝑅 |
26 | | df-rn 4622 |
. . . . . . 7
⊢ ran
(𝑆 ∘ ◡(inr ↾ dom 𝑆)) = dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)) |
27 | | rncoss 4881 |
. . . . . . 7
⊢ ran
(𝑆 ∘ ◡(inr ↾ dom 𝑆)) ⊆ ran 𝑆 |
28 | 26, 27 | eqsstrri 3180 |
. . . . . 6
⊢ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)) ⊆ ran 𝑆 |
29 | | ss2in 3355 |
. . . . . 6
⊢ ((dom
◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ⊆ ran 𝑅 ∧ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)) ⊆ ran 𝑆) → (dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) ⊆ (ran 𝑅 ∩ ran 𝑆)) |
30 | 25, 28, 29 | mp2an 424 |
. . . . 5
⊢ (dom
◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) ⊆ (ran 𝑅 ∩ ran 𝑆) |
31 | | djuinj.disj |
. . . . 5
⊢ (𝜑 → (ran 𝑅 ∩ ran 𝑆) = ∅) |
32 | 30, 31 | sseqtrid 3197 |
. . . 4
⊢ (𝜑 → (dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) ⊆ ∅) |
33 | | ss0 3455 |
. . . 4
⊢ ((dom
◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) ⊆ ∅ → (dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) = ∅) |
34 | 32, 33 | syl 14 |
. . 3
⊢ (𝜑 → (dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) = ∅) |
35 | | funun 5242 |
. . 3
⊢ (((Fun
◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∧ Fun ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) ∧ (dom ◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∩ dom ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) = ∅) → Fun (◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)))) |
36 | 11, 22, 34, 35 | syl21anc 1232 |
. 2
⊢ (𝜑 → Fun (◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)))) |
37 | | df-djud 7080 |
. . . . 5
⊢ (𝑅 ⊔d 𝑆) = ((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
38 | 37 | cnveqi 4786 |
. . . 4
⊢ ◡(𝑅 ⊔d 𝑆) = ◡((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
39 | | cnvun 5016 |
. . . 4
⊢ ◡((𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ (𝑆 ∘ ◡(inr ↾ dom 𝑆))) = (◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
40 | 38, 39 | eqtri 2191 |
. . 3
⊢ ◡(𝑅 ⊔d 𝑆) = (◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆))) |
41 | 40 | funeqi 5219 |
. 2
⊢ (Fun
◡(𝑅 ⊔d 𝑆) ↔ Fun (◡(𝑅 ∘ ◡(inl ↾ dom 𝑅)) ∪ ◡(𝑆 ∘ ◡(inr ↾ dom 𝑆)))) |
42 | 36, 41 | sylibr 133 |
1
⊢ (𝜑 → Fun ◡(𝑅 ⊔d 𝑆)) |