Proof of Theorem caseinl
Step | Hyp | Ref
| Expression |
1 | | df-case 7057 |
. . . 4
⊢
case(𝐹, 𝐺) = ((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr)) |
2 | 1 | fveq1i 5495 |
. . 3
⊢
(case(𝐹, 𝐺)‘(inl‘𝐴)) = (((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))‘(inl‘𝐴)) |
3 | | caseinl.f |
. . . . . . 7
⊢ (𝜑 → 𝐹 Fn 𝐵) |
4 | | fnfun 5293 |
. . . . . . 7
⊢ (𝐹 Fn 𝐵 → Fun 𝐹) |
5 | 3, 4 | syl 14 |
. . . . . 6
⊢ (𝜑 → Fun 𝐹) |
6 | | djulf1o 7031 |
. . . . . . . 8
⊢
inl:V–1-1-onto→({∅} × V) |
7 | | f1ocnv 5453 |
. . . . . . . 8
⊢
(inl:V–1-1-onto→({∅} × V) → ◡inl:({∅} × V)–1-1-onto→V) |
8 | 6, 7 | ax-mp 5 |
. . . . . . 7
⊢ ◡inl:({∅} × V)–1-1-onto→V |
9 | | f1ofun 5442 |
. . . . . . 7
⊢ (◡inl:({∅} × V)–1-1-onto→V → Fun ◡inl) |
10 | 8, 9 | ax-mp 5 |
. . . . . 6
⊢ Fun ◡inl |
11 | | funco 5236 |
. . . . . 6
⊢ ((Fun
𝐹 ∧ Fun ◡inl) → Fun (𝐹 ∘ ◡inl)) |
12 | 5, 10, 11 | sylancl 411 |
. . . . 5
⊢ (𝜑 → Fun (𝐹 ∘ ◡inl)) |
13 | | dmco 5117 |
. . . . . 6
⊢ dom
(𝐹 ∘ ◡inl) = (◡◡inl
“ dom 𝐹) |
14 | | df-inl 7020 |
. . . . . . . . . . 11
⊢ inl =
(𝑥 ∈ V ↦
〈∅, 𝑥〉) |
15 | 14 | funmpt2 5235 |
. . . . . . . . . 10
⊢ Fun
inl |
16 | | funrel 5213 |
. . . . . . . . . 10
⊢ (Fun inl
→ Rel inl) |
17 | 15, 16 | ax-mp 5 |
. . . . . . . . 9
⊢ Rel
inl |
18 | | dfrel2 5059 |
. . . . . . . . 9
⊢ (Rel inl
↔ ◡◡inl = inl) |
19 | 17, 18 | mpbi 144 |
. . . . . . . 8
⊢ ◡◡inl
= inl |
20 | 19 | a1i 9 |
. . . . . . 7
⊢ (𝜑 → ◡◡inl
= inl) |
21 | | fndm 5295 |
. . . . . . . 8
⊢ (𝐹 Fn 𝐵 → dom 𝐹 = 𝐵) |
22 | 3, 21 | syl 14 |
. . . . . . 7
⊢ (𝜑 → dom 𝐹 = 𝐵) |
23 | 20, 22 | imaeq12d 4952 |
. . . . . 6
⊢ (𝜑 → (◡◡inl
“ dom 𝐹) = (inl
“ 𝐵)) |
24 | 13, 23 | eqtrid 2215 |
. . . . 5
⊢ (𝜑 → dom (𝐹 ∘ ◡inl) = (inl “ 𝐵)) |
25 | | df-fn 5199 |
. . . . 5
⊢ ((𝐹 ∘ ◡inl) Fn (inl “ 𝐵) ↔ (Fun (𝐹 ∘ ◡inl) ∧ dom (𝐹 ∘ ◡inl) = (inl “ 𝐵))) |
26 | 12, 24, 25 | sylanbrc 415 |
. . . 4
⊢ (𝜑 → (𝐹 ∘ ◡inl) Fn (inl “ 𝐵)) |
27 | | caseinl.g |
. . . . . 6
⊢ (𝜑 → Fun 𝐺) |
28 | | djurf1o 7032 |
. . . . . . . 8
⊢
inr:V–1-1-onto→({1o} × V) |
29 | | f1ocnv 5453 |
. . . . . . . 8
⊢
(inr:V–1-1-onto→({1o} × V) → ◡inr:({1o} × V)–1-1-onto→V) |
30 | 28, 29 | ax-mp 5 |
. . . . . . 7
⊢ ◡inr:({1o} × V)–1-1-onto→V |
31 | | f1ofun 5442 |
. . . . . . 7
⊢ (◡inr:({1o} × V)–1-1-onto→V → Fun ◡inr) |
32 | 30, 31 | ax-mp 5 |
. . . . . 6
⊢ Fun ◡inr |
33 | | funco 5236 |
. . . . . 6
⊢ ((Fun
𝐺 ∧ Fun ◡inr) → Fun (𝐺 ∘ ◡inr)) |
34 | 27, 32, 33 | sylancl 411 |
. . . . 5
⊢ (𝜑 → Fun (𝐺 ∘ ◡inr)) |
35 | | dmco 5117 |
. . . . . . 7
⊢ dom
(𝐺 ∘ ◡inr) = (◡◡inr
“ dom 𝐺) |
36 | | imacnvcnv 5073 |
. . . . . . 7
⊢ (◡◡inr
“ dom 𝐺) = (inr
“ dom 𝐺) |
37 | 35, 36 | eqtri 2191 |
. . . . . 6
⊢ dom
(𝐺 ∘ ◡inr) = (inr “ dom 𝐺) |
38 | 37 | a1i 9 |
. . . . 5
⊢ (𝜑 → dom (𝐺 ∘ ◡inr) = (inr “ dom 𝐺)) |
39 | | df-fn 5199 |
. . . . 5
⊢ ((𝐺 ∘ ◡inr) Fn (inr “ dom 𝐺) ↔ (Fun (𝐺 ∘ ◡inr) ∧ dom (𝐺 ∘ ◡inr) = (inr “ dom 𝐺))) |
40 | 34, 38, 39 | sylanbrc 415 |
. . . 4
⊢ (𝜑 → (𝐺 ∘ ◡inr) Fn (inr “ dom 𝐺)) |
41 | | djuin 7037 |
. . . . 5
⊢ ((inl
“ 𝐵) ∩ (inr
“ dom 𝐺)) =
∅ |
42 | 41 | a1i 9 |
. . . 4
⊢ (𝜑 → ((inl “ 𝐵) ∩ (inr “ dom 𝐺)) = ∅) |
43 | | caseinl.a |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈ 𝐵) |
44 | 43 | elexd 2743 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ V) |
45 | | f1odm 5444 |
. . . . . . . 8
⊢
(inl:V–1-1-onto→({∅} × V) → dom inl =
V) |
46 | 6, 45 | ax-mp 5 |
. . . . . . 7
⊢ dom inl =
V |
47 | 44, 46 | eleqtrrdi 2264 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ dom inl) |
48 | 47, 15 | jctil 310 |
. . . . 5
⊢ (𝜑 → (Fun inl ∧ 𝐴 ∈ dom
inl)) |
49 | | funfvima 5724 |
. . . . 5
⊢ ((Fun inl
∧ 𝐴 ∈ dom inl)
→ (𝐴 ∈ 𝐵 → (inl‘𝐴) ∈ (inl “ 𝐵))) |
50 | 48, 43, 49 | sylc 62 |
. . . 4
⊢ (𝜑 → (inl‘𝐴) ∈ (inl “ 𝐵)) |
51 | | fvun1 5560 |
. . . 4
⊢ (((𝐹 ∘ ◡inl) Fn (inl “ 𝐵) ∧ (𝐺 ∘ ◡inr) Fn (inr “ dom 𝐺) ∧ (((inl “ 𝐵) ∩ (inr “ dom 𝐺)) = ∅ ∧ (inl‘𝐴) ∈ (inl “ 𝐵))) → (((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))‘(inl‘𝐴)) = ((𝐹 ∘ ◡inl)‘(inl‘𝐴))) |
52 | 26, 40, 42, 50, 51 | syl112anc 1237 |
. . 3
⊢ (𝜑 → (((𝐹 ∘ ◡inl) ∪ (𝐺 ∘ ◡inr))‘(inl‘𝐴)) = ((𝐹 ∘ ◡inl)‘(inl‘𝐴))) |
53 | 2, 52 | eqtrid 2215 |
. 2
⊢ (𝜑 → (case(𝐹, 𝐺)‘(inl‘𝐴)) = ((𝐹 ∘ ◡inl)‘(inl‘𝐴))) |
54 | | f1ofn 5441 |
. . . 4
⊢ (◡inl:({∅} × V)–1-1-onto→V → ◡inl Fn ({∅} ×
V)) |
55 | 8, 54 | ax-mp 5 |
. . 3
⊢ ◡inl Fn ({∅} ×
V) |
56 | | f1of 5440 |
. . . . . 6
⊢
(inl:V–1-1-onto→({∅} × V) →
inl:V⟶({∅} × V)) |
57 | 6, 56 | ax-mp 5 |
. . . . 5
⊢
inl:V⟶({∅} × V) |
58 | 57 | a1i 9 |
. . . 4
⊢ (𝜑 → inl:V⟶({∅}
× V)) |
59 | 58, 44 | ffvelrnd 5629 |
. . 3
⊢ (𝜑 → (inl‘𝐴) ∈ ({∅} ×
V)) |
60 | | fvco2 5563 |
. . 3
⊢ ((◡inl Fn ({∅} × V) ∧
(inl‘𝐴) ∈
({∅} × V)) → ((𝐹 ∘ ◡inl)‘(inl‘𝐴)) = (𝐹‘(◡inl‘(inl‘𝐴)))) |
61 | 55, 59, 60 | sylancr 412 |
. 2
⊢ (𝜑 → ((𝐹 ∘ ◡inl)‘(inl‘𝐴)) = (𝐹‘(◡inl‘(inl‘𝐴)))) |
62 | | f1ocnvfv1 5753 |
. . . 4
⊢
((inl:V–1-1-onto→({∅} × V) ∧ 𝐴 ∈ V) → (◡inl‘(inl‘𝐴)) = 𝐴) |
63 | 6, 44, 62 | sylancr 412 |
. . 3
⊢ (𝜑 → (◡inl‘(inl‘𝐴)) = 𝐴) |
64 | 63 | fveq2d 5498 |
. 2
⊢ (𝜑 → (𝐹‘(◡inl‘(inl‘𝐴))) = (𝐹‘𝐴)) |
65 | 53, 61, 64 | 3eqtrd 2207 |
1
⊢ (𝜑 → (case(𝐹, 𝐺)‘(inl‘𝐴)) = (𝐹‘𝐴)) |