Proof of Theorem djufun
Step | Hyp | Ref
| Expression |
1 | | djufun.f |
. . . 4
⊢ (𝜑 → Fun 𝐹) |
2 | | inlresf1 7018 |
. . . . 5
⊢ (inl
↾ dom 𝐹):dom 𝐹–1-1→(dom 𝐹 ⊔ dom 𝐺) |
3 | | df-f1 5188 |
. . . . . 6
⊢ ((inl
↾ dom 𝐹):dom 𝐹–1-1→(dom 𝐹 ⊔ dom 𝐺) ↔ ((inl ↾ dom 𝐹):dom 𝐹⟶(dom 𝐹 ⊔ dom 𝐺) ∧ Fun ◡(inl ↾ dom 𝐹))) |
4 | 3 | simprbi 273 |
. . . . 5
⊢ ((inl
↾ dom 𝐹):dom 𝐹–1-1→(dom 𝐹 ⊔ dom 𝐺) → Fun ◡(inl ↾ dom 𝐹)) |
5 | 2, 4 | mp1i 10 |
. . . 4
⊢ (𝜑 → Fun ◡(inl ↾ dom 𝐹)) |
6 | | funco 5223 |
. . . 4
⊢ ((Fun
𝐹 ∧ Fun ◡(inl ↾ dom 𝐹)) → Fun (𝐹 ∘ ◡(inl ↾ dom 𝐹))) |
7 | 1, 5, 6 | syl2anc 409 |
. . 3
⊢ (𝜑 → Fun (𝐹 ∘ ◡(inl ↾ dom 𝐹))) |
8 | | djufun.g |
. . . 4
⊢ (𝜑 → Fun 𝐺) |
9 | | inrresf1 7019 |
. . . . 5
⊢ (inr
↾ dom 𝐺):dom 𝐺–1-1→(dom 𝐹 ⊔ dom 𝐺) |
10 | | df-f1 5188 |
. . . . . 6
⊢ ((inr
↾ dom 𝐺):dom 𝐺–1-1→(dom 𝐹 ⊔ dom 𝐺) ↔ ((inr ↾ dom 𝐺):dom 𝐺⟶(dom 𝐹 ⊔ dom 𝐺) ∧ Fun ◡(inr ↾ dom 𝐺))) |
11 | 10 | simprbi 273 |
. . . . 5
⊢ ((inr
↾ dom 𝐺):dom 𝐺–1-1→(dom 𝐹 ⊔ dom 𝐺) → Fun ◡(inr ↾ dom 𝐺)) |
12 | 9, 11 | mp1i 10 |
. . . 4
⊢ (𝜑 → Fun ◡(inr ↾ dom 𝐺)) |
13 | | funco 5223 |
. . . 4
⊢ ((Fun
𝐺 ∧ Fun ◡(inr ↾ dom 𝐺)) → Fun (𝐺 ∘ ◡(inr ↾ dom 𝐺))) |
14 | 8, 12, 13 | syl2anc 409 |
. . 3
⊢ (𝜑 → Fun (𝐺 ∘ ◡(inr ↾ dom 𝐺))) |
15 | | dmcoss 4868 |
. . . . . . 7
⊢ dom
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ⊆ dom ◡(inl ↾ dom 𝐹) |
16 | | df-rn 4610 |
. . . . . . 7
⊢ ran (inl
↾ dom 𝐹) = dom ◡(inl ↾ dom 𝐹) |
17 | 15, 16 | sseqtrri 3173 |
. . . . . 6
⊢ dom
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ⊆ ran (inl ↾ dom 𝐹) |
18 | | dmcoss 4868 |
. . . . . . 7
⊢ dom
(𝐺 ∘ ◡(inr ↾ dom 𝐺)) ⊆ dom ◡(inr ↾ dom 𝐺) |
19 | | df-rn 4610 |
. . . . . . 7
⊢ ran (inr
↾ dom 𝐺) = dom ◡(inr ↾ dom 𝐺) |
20 | 18, 19 | sseqtrri 3173 |
. . . . . 6
⊢ dom
(𝐺 ∘ ◡(inr ↾ dom 𝐺)) ⊆ ran (inr ↾ dom 𝐺) |
21 | | ss2in 3346 |
. . . . . 6
⊢ ((dom
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ⊆ ran (inl ↾ dom 𝐹) ∧ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺)) ⊆ ran (inr ↾ dom 𝐺)) → (dom (𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) ⊆ (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom
𝐺))) |
22 | 17, 20, 21 | mp2an 423 |
. . . . 5
⊢ (dom
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) ⊆ (ran (inl ↾ dom 𝐹) ∩ ran (inr ↾ dom
𝐺)) |
23 | | djuinr 7020 |
. . . . . 6
⊢ (ran (inl
↾ dom 𝐹) ∩ ran
(inr ↾ dom 𝐺)) =
∅ |
24 | 23 | a1i 9 |
. . . . 5
⊢ (𝜑 → (ran (inl ↾ dom
𝐹) ∩ ran (inr ↾
dom 𝐺)) =
∅) |
25 | 22, 24 | sseqtrid 3188 |
. . . 4
⊢ (𝜑 → (dom (𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) ⊆ ∅) |
26 | | ss0 3445 |
. . . 4
⊢ ((dom
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) ⊆ ∅ → (dom (𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) = ∅) |
27 | 25, 26 | syl 14 |
. . 3
⊢ (𝜑 → (dom (𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) = ∅) |
28 | | funun 5227 |
. . 3
⊢ (((Fun
(𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∧ Fun (𝐺 ∘ ◡(inr ↾ dom 𝐺))) ∧ (dom (𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∩ dom (𝐺 ∘ ◡(inr ↾ dom 𝐺))) = ∅) → Fun ((𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∪ (𝐺 ∘ ◡(inr ↾ dom 𝐺)))) |
29 | 7, 14, 27, 28 | syl21anc 1226 |
. 2
⊢ (𝜑 → Fun ((𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∪ (𝐺 ∘ ◡(inr ↾ dom 𝐺)))) |
30 | | df-djud 7060 |
. . 3
⊢ (𝐹 ⊔d 𝐺) = ((𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∪ (𝐺 ∘ ◡(inr ↾ dom 𝐺))) |
31 | 30 | funeqi 5204 |
. 2
⊢ (Fun
(𝐹 ⊔d
𝐺) ↔ Fun ((𝐹 ∘ ◡(inl ↾ dom 𝐹)) ∪ (𝐺 ∘ ◡(inr ↾ dom 𝐺)))) |
32 | 29, 31 | sylibr 133 |
1
⊢ (𝜑 → Fun (𝐹 ⊔d 𝐺)) |