Step | Hyp | Ref
| Expression |
1 | | relfunc 16729 |
. . 3
⊢ Rel
(𝐷 Func 𝐷) |
2 | | ressffth.d |
. . . . 5
⊢ 𝐷 = (𝐶 ↾s 𝑆) |
3 | | resscat 16719 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) |
4 | 2, 3 | syl5eqel 2854 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 ∈ Cat) |
5 | | ressffth.i |
. . . . 5
⊢ 𝐼 =
(idfunc‘𝐷) |
6 | 5 | idfucl 16748 |
. . . 4
⊢ (𝐷 ∈ Cat → 𝐼 ∈ (𝐷 Func 𝐷)) |
7 | 4, 6 | syl 17 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ (𝐷 Func 𝐷)) |
8 | | 1st2nd 7367 |
. . 3
⊢ ((Rel
(𝐷 Func 𝐷) ∧ 𝐼 ∈ (𝐷 Func 𝐷)) → 𝐼 = 〈(1st ‘𝐼), (2nd ‘𝐼)〉) |
9 | 1, 7, 8 | sylancr 575 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 = 〈(1st ‘𝐼), (2nd ‘𝐼)〉) |
10 | | eqidd 2772 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘𝐷)) |
11 | | eqidd 2772 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘𝐷)) |
12 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘𝐶) |
13 | 12 | ressinbas 16143 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
14 | 13 | adantl 467 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
15 | 2, 14 | syl5eq 2817 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
16 | 15 | fveq2d 6337 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶))))) |
17 | | eqid 2771 |
. . . . . . . . . . . 12
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) |
18 | | simpl 468 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐶 ∈ Cat) |
19 | | inss2 3982 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶) |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶)) |
21 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) |
22 | | eqid 2771 |
. . . . . . . . . . . 12
⊢ (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) = (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) |
23 | 12, 17, 18, 20, 21, 22 | fullresc 16718 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ((Homf
‘(𝐶
↾s (𝑆
∩ (Base‘𝐶)))) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ∧
(compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))) |
24 | 23 | simpld 482 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘(𝐶
↾s (𝑆
∩ (Base‘𝐶)))) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
25 | 16, 24 | eqtrd 2805 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
26 | 15 | fveq2d 6337 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶))))) |
27 | 23 | simprd 483 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
28 | 26, 27 | eqtrd 2805 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
29 | | ovex 6827 |
. . . . . . . . . . 11
⊢ (𝐶 ↾s 𝑆) ∈ V |
30 | 2, 29 | eqeltri 2846 |
. . . . . . . . . 10
⊢ 𝐷 ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 ∈ V) |
32 | | ovex 6827 |
. . . . . . . . . 10
⊢ (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) ∈ V |
33 | 32 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) ∈ V) |
34 | 10, 11, 25, 28, 31, 31, 31, 33 | funcpropd 16767 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐷 Func 𝐷) = (𝐷 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
35 | 12, 17, 18, 20 | fullsubc 16717 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ((Homf
‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))) ∈ (Subcat‘𝐶)) |
36 | | funcres2 16765 |
. . . . . . . . 9
⊢
(((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))) ∈ (Subcat‘𝐶) → (𝐷 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ⊆ (𝐷 Func 𝐶)) |
37 | 35, 36 | syl 17 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐷 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ⊆ (𝐷 Func 𝐶)) |
38 | 34, 37 | eqsstrd 3788 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐷 Func 𝐷) ⊆ (𝐷 Func 𝐶)) |
39 | 38, 7 | sseldd 3753 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ (𝐷 Func 𝐶)) |
40 | 9, 39 | eqeltrrd 2851 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐷 Func 𝐶)) |
41 | | df-br 4788 |
. . . . 5
⊢
((1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐷 Func 𝐶)) |
42 | 40, 41 | sylibr 224 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼)) |
43 | | f1oi 6316 |
. . . . . 6
⊢ ( I
↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦) |
44 | | eqid 2771 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
45 | 4 | adantr 466 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐷 ∈ Cat) |
46 | | eqid 2771 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
47 | | simprl 754 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐷)) |
48 | | simprr 756 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷)) |
49 | 5, 44, 45, 46, 47, 48 | idfu2nd 16744 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd ‘𝐼)𝑦) = ( I ↾ (𝑥(Hom ‘𝐷)𝑦))) |
50 | | eqidd 2772 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
51 | | eqid 2771 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
52 | 2, 51 | resshom 16286 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑉 → (Hom ‘𝐶) = (Hom ‘𝐷)) |
53 | 52 | ad2antlr 706 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐶) = (Hom ‘𝐷)) |
54 | 5, 44, 45, 47 | idfu1 16747 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st ‘𝐼)‘𝑥) = 𝑥) |
55 | 5, 44, 45, 48 | idfu1 16747 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st ‘𝐼)‘𝑦) = 𝑦) |
56 | 53, 54, 55 | oveq123d 6817 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) = (𝑥(Hom ‘𝐷)𝑦)) |
57 | 49, 50, 56 | f1oeq123d 6275 |
. . . . . 6
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) ↔ ( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦))) |
58 | 43, 57 | mpbiri 248 |
. . . . 5
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) |
59 | 58 | ralrimivva 3120 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) |
60 | 44, 46, 51 | isffth2 16783 |
. . . 4
⊢
((1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼) ↔ ((1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼) ∧ ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)))) |
61 | 42, 59, 60 | sylanbrc 572 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼)) |
62 | | df-br 4788 |
. . 3
⊢
((1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |
63 | 61, 62 | sylib 208 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |
64 | 9, 63 | eqeltrd 2850 |
1
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |