Step | Hyp | Ref
| Expression |
1 | | relfunc 16345 |
. . 3
⊢ Rel
(𝐷 Func 𝐷) |
2 | | ressffth.d |
. . . . 5
⊢ 𝐷 = (𝐶 ↾s 𝑆) |
3 | | resscat 16335 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) ∈ Cat) |
4 | 2, 3 | syl5eqel 2692 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 ∈ Cat) |
5 | | ressffth.i |
. . . . 5
⊢ 𝐼 =
(idfunc‘𝐷) |
6 | 5 | idfucl 16364 |
. . . 4
⊢ (𝐷 ∈ Cat → 𝐼 ∈ (𝐷 Func 𝐷)) |
7 | 4, 6 | syl 17 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ (𝐷 Func 𝐷)) |
8 | | 1st2nd 7105 |
. . 3
⊢ ((Rel
(𝐷 Func 𝐷) ∧ 𝐼 ∈ (𝐷 Func 𝐷)) → 𝐼 = 〈(1st ‘𝐼), (2nd ‘𝐼)〉) |
9 | 1, 7, 8 | sylancr 694 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 = 〈(1st ‘𝐼), (2nd ‘𝐼)〉) |
10 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘𝐷)) |
11 | | eqidd 2611 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘𝐷)) |
12 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(Base‘𝐶) =
(Base‘𝐶) |
13 | 12 | ressinbas 15763 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∈ 𝑉 → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
14 | 13 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐶 ↾s 𝑆) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
15 | 2, 14 | syl5eq 2656 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) |
16 | 15 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶))))) |
17 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Homf ‘𝐶) = (Homf ‘𝐶) |
18 | | simpl 472 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐶 ∈ Cat) |
19 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢ (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶) |
20 | 19 | a1i 11 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝑆 ∩ (Base‘𝐶)) ⊆ (Base‘𝐶)) |
21 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) = (𝐶 ↾s (𝑆 ∩ (Base‘𝐶))) |
22 | | eqid 2610 |
. . . . . . . . . . . 12
⊢ (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) = (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))) |
23 | 12, 17, 18, 20, 21, 22 | fullresc 16334 |
. . . . . . . . . . 11
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ((Homf
‘(𝐶
↾s (𝑆
∩ (Base‘𝐶)))) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))) ∧
(compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))))))) |
24 | 23 | simpld 474 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘(𝐶
↾s (𝑆
∩ (Base‘𝐶)))) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
25 | 16, 24 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (Homf
‘𝐷) =
(Homf ‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
26 | 15 | fveq2d 6107 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶))))) |
27 | 23 | simprd 478 |
. . . . . . . . . 10
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘(𝐶 ↾s (𝑆 ∩ (Base‘𝐶)))) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
28 | 26, 27 | eqtrd 2644 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) →
(compf‘𝐷) = (compf‘(𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
29 | | ovex 6577 |
. . . . . . . . . . 11
⊢ (𝐶 ↾s 𝑆) ∈ V |
30 | 2, 29 | eqeltri 2684 |
. . . . . . . . . 10
⊢ 𝐷 ∈ V |
31 | 30 | a1i 11 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐷 ∈ V) |
32 | | ovex 6577 |
. . . . . . . . . 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 16383 |
. . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐷 Func 𝐷) = (𝐷 Func (𝐶 ↾cat
((Homf ‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶))))))) |
35 | 12, 17, 18, 20 | fullsubc 16333 |
. . . . . . . . 9
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ((Homf
‘𝐶) ↾ ((𝑆 ∩ (Base‘𝐶)) × (𝑆 ∩ (Base‘𝐶)))) ∈ (Subcat‘𝐶)) |
36 | | funcres2 16381 |
. . . . . . . . 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 3602 |
. . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (𝐷 Func 𝐷) ⊆ (𝐷 Func 𝐶)) |
39 | 38, 7 | sseldd 3569 |
. . . . . 6
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ (𝐷 Func 𝐶)) |
40 | 9, 39 | eqeltrrd 2689 |
. . . . 5
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐷 Func 𝐶)) |
41 | | df-br 4584 |
. . . . 5
⊢
((1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐷 Func 𝐶)) |
42 | 40, 41 | sylibr 223 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼)) |
43 | | f1oi 6086 |
. . . . . 6
⊢ ( I
↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦) |
44 | | eqid 2610 |
. . . . . . . 8
⊢
(Base‘𝐷) =
(Base‘𝐷) |
45 | 4 | adantr 480 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝐷 ∈ Cat) |
46 | | eqid 2610 |
. . . . . . . 8
⊢ (Hom
‘𝐷) = (Hom
‘𝐷) |
47 | | simprl 790 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑥 ∈ (Base‘𝐷)) |
48 | | simprr 792 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → 𝑦 ∈ (Base‘𝐷)) |
49 | 5, 44, 45, 46, 47, 48 | idfu2nd 16360 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd ‘𝐼)𝑦) = ( I ↾ (𝑥(Hom ‘𝐷)𝑦))) |
50 | | eqidd 2611 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(Hom ‘𝐷)𝑦) = (𝑥(Hom ‘𝐷)𝑦)) |
51 | | eqid 2610 |
. . . . . . . . . 10
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
52 | 2, 51 | resshom 15901 |
. . . . . . . . 9
⊢ (𝑆 ∈ 𝑉 → (Hom ‘𝐶) = (Hom ‘𝐷)) |
53 | 52 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (Hom ‘𝐶) = (Hom ‘𝐷)) |
54 | 5, 44, 45, 47 | idfu1 16363 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st ‘𝐼)‘𝑥) = 𝑥) |
55 | 5, 44, 45, 48 | idfu1 16363 |
. . . . . . . 8
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((1st ‘𝐼)‘𝑦) = 𝑦) |
56 | 53, 54, 55 | oveq123d 6570 |
. . . . . . 7
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) = (𝑥(Hom ‘𝐷)𝑦)) |
57 | 49, 50, 56 | f1oeq123d 6046 |
. . . . . 6
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → ((𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) ↔ ( I ↾ (𝑥(Hom ‘𝐷)𝑦)):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(𝑥(Hom ‘𝐷)𝑦))) |
58 | 43, 57 | mpbiri 247 |
. . . . 5
⊢ (((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) ∧ (𝑥 ∈ (Base‘𝐷) ∧ 𝑦 ∈ (Base‘𝐷))) → (𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) |
59 | 58 | ralrimivva 2954 |
. . . 4
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) |
60 | 44, 46, 51 | isffth2 16399 |
. . . 4
⊢
((1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼) ↔ ((1st ‘𝐼)(𝐷 Func 𝐶)(2nd ‘𝐼) ∧ ∀𝑥 ∈ (Base‘𝐷)∀𝑦 ∈ (Base‘𝐷)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐷)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)))) |
61 | 42, 59, 60 | sylanbrc 695 |
. . 3
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → (1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼)) |
62 | | df-br 4584 |
. . 3
⊢
((1st ‘𝐼)((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |
63 | 61, 62 | sylib 207 |
. 2
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |
64 | 9, 63 | eqeltrd 2688 |
1
⊢ ((𝐶 ∈ Cat ∧ 𝑆 ∈ 𝑉) → 𝐼 ∈ ((𝐷 Full 𝐶) ∩ (𝐷 Faith 𝐶))) |