Step | Hyp | Ref
| Expression |
1 | | relfunc 17368 |
. . 3
⊢ Rel
(𝐶 Func 𝐸) |
2 | | fullfunc 17413 |
. . . . 5
⊢ (𝐶 Full 𝐷) ⊆ (𝐶 Func 𝐷) |
3 | | cofull.f |
. . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐶 Full 𝐷)) |
4 | 2, 3 | sseldi 3899 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) |
5 | | fullfunc 17413 |
. . . . 5
⊢ (𝐷 Full 𝐸) ⊆ (𝐷 Func 𝐸) |
6 | | cofull.g |
. . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐷 Full 𝐸)) |
7 | 5, 6 | sseldi 3899 |
. . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) |
8 | 4, 7 | cofucl 17394 |
. . 3
⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) |
9 | | 1st2nd 7810 |
. . 3
⊢ ((Rel
(𝐶 Func 𝐸) ∧ (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) → (𝐺 ∘func 𝐹) = 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉) |
10 | 1, 8, 9 | sylancr 590 |
. 2
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉) |
11 | | 1st2ndbr 7813 |
. . . . 5
⊢ ((Rel
(𝐶 Func 𝐸) ∧ (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) → (1st ‘(𝐺 ∘func
𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) |
12 | 1, 8, 11 | sylancr 590 |
. . . 4
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) |
13 | | eqid 2737 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
14 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐸) = (Hom
‘𝐸) |
15 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
16 | | relfull 17415 |
. . . . . . . . 9
⊢ Rel
(𝐷 Full 𝐸) |
17 | 6 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Full 𝐸)) |
18 | | 1st2ndbr 7813 |
. . . . . . . . 9
⊢ ((Rel
(𝐷 Full 𝐸) ∧ 𝐺 ∈ (𝐷 Full 𝐸)) → (1st ‘𝐺)(𝐷 Full 𝐸)(2nd ‘𝐺)) |
19 | 16, 17, 18 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Full 𝐸)(2nd ‘𝐺)) |
20 | | eqid 2737 |
. . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) |
21 | | relfunc 17368 |
. . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐷) |
22 | 4 | adantr 484 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷)) |
23 | | 1st2ndbr 7813 |
. . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
24 | 21, 22, 23 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) |
25 | 20, 13, 24 | funcf1 17372 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) |
26 | | simprl 771 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) |
27 | 25, 26 | ffvelrnd 6905 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) |
28 | | simprr 773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) |
29 | 25, 28 | ffvelrnd 6905 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) |
30 | 13, 14, 15, 19, 27, 29 | fullfo 17419 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))–onto→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
31 | | eqid 2737 |
. . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
32 | | relfull 17415 |
. . . . . . . . 9
⊢ Rel
(𝐶 Full 𝐷) |
33 | 3 | adantr 484 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Full 𝐷)) |
34 | | 1st2ndbr 7813 |
. . . . . . . . 9
⊢ ((Rel
(𝐶 Full 𝐷) ∧ 𝐹 ∈ (𝐶 Full 𝐷)) → (1st ‘𝐹)(𝐶 Full 𝐷)(2nd ‘𝐹)) |
35 | 32, 33, 34 | sylancr 590 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Full 𝐷)(2nd ‘𝐹)) |
36 | 20, 15, 31, 35, 26, 28 | fullfo 17419 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) |
37 | | foco 6647 |
. . . . . . 7
⊢
(((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))–onto→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∧ (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
38 | 30, 36, 37 | syl2anc 587 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
39 | 7 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸)) |
40 | 20, 22, 39, 26, 28 | cofu2nd 17391 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
41 | | eqidd 2738 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑦)) |
42 | 20, 22, 39, 26 | cofu1 17390 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑥) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥))) |
43 | 20, 22, 39, 28 | cofu1 17390 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑦) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))) |
44 | 42, 43 | oveq12d 7231 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) |
45 | 40, 41, 44 | foeq123d 6654 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↔ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))) |
46 | 38, 45 | mpbird 260 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦))) |
47 | 46 | ralrimivva 3112 |
. . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦))) |
48 | 20, 14, 31 | isfull2 17418 |
. . . 4
⊢
((1st ‘(𝐺 ∘func 𝐹))(𝐶 Full 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ((1st
‘(𝐺
∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–onto→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)))) |
49 | 12, 47, 48 | sylanbrc 586 |
. . 3
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹))(𝐶 Full 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) |
50 | | df-br 5054 |
. . 3
⊢
((1st ‘(𝐺 ∘func 𝐹))(𝐶 Full 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Full 𝐸)) |
51 | 49, 50 | sylib 221 |
. 2
⊢ (𝜑 → 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Full 𝐸)) |
52 | 10, 51 | eqeltrd 2838 |
1
⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Full 𝐸)) |