| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relfunc 17907 | . . 3
⊢ Rel
(𝐶 Func 𝐶) | 
| 2 |  | idffth.i | . . . 4
⊢ 𝐼 =
(idfunc‘𝐶) | 
| 3 | 2 | idfucl 17926 | . . 3
⊢ (𝐶 ∈ Cat → 𝐼 ∈ (𝐶 Func 𝐶)) | 
| 4 |  | 1st2nd 8064 | . . 3
⊢ ((Rel
(𝐶 Func 𝐶) ∧ 𝐼 ∈ (𝐶 Func 𝐶)) → 𝐼 = 〈(1st ‘𝐼), (2nd ‘𝐼)〉) | 
| 5 | 1, 3, 4 | sylancr 587 | . 2
⊢ (𝐶 ∈ Cat → 𝐼 = 〈(1st
‘𝐼), (2nd
‘𝐼)〉) | 
| 6 | 5, 3 | eqeltrrd 2842 | . . . . 5
⊢ (𝐶 ∈ Cat →
〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐶 Func 𝐶)) | 
| 7 |  | df-br 5144 | . . . . 5
⊢
((1st ‘𝐼)(𝐶 Func 𝐶)(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ (𝐶 Func 𝐶)) | 
| 8 | 6, 7 | sylibr 234 | . . . 4
⊢ (𝐶 ∈ Cat →
(1st ‘𝐼)(𝐶 Func 𝐶)(2nd ‘𝐼)) | 
| 9 |  | f1oi 6886 | . . . . . 6
⊢ ( I
↾ (𝑥(Hom ‘𝐶)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(𝑥(Hom ‘𝐶)𝑦) | 
| 10 |  | eqid 2737 | . . . . . . . 8
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 11 |  | simpl 482 | . . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐶 ∈ Cat) | 
| 12 |  | eqid 2737 | . . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 13 |  | simprl 771 | . . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) | 
| 14 |  | simprr 773 | . . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) | 
| 15 | 2, 10, 11, 12, 13, 14 | idfu2nd 17922 | . . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐼)𝑦) = ( I ↾ (𝑥(Hom ‘𝐶)𝑦))) | 
| 16 |  | eqidd 2738 | . . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑦)) | 
| 17 | 2, 10, 11, 13 | idfu1 17925 | . . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐼)‘𝑥) = 𝑥) | 
| 18 | 2, 10, 11, 14 | idfu1 17925 | . . . . . . . 8
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐼)‘𝑦) = 𝑦) | 
| 19 | 17, 18 | oveq12d 7449 | . . . . . . 7
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) = (𝑥(Hom ‘𝐶)𝑦)) | 
| 20 | 15, 16, 19 | f1oeq123d 6842 | . . . . . 6
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)) ↔ ( I ↾ (𝑥(Hom ‘𝐶)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(𝑥(Hom ‘𝐶)𝑦))) | 
| 21 | 9, 20 | mpbiri 258 | . . . . 5
⊢ ((𝐶 ∈ Cat ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) | 
| 22 | 21 | ralrimivva 3202 | . . . 4
⊢ (𝐶 ∈ Cat → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦))) | 
| 23 | 10, 12, 12 | isffth2 17963 | . . . 4
⊢
((1st ‘𝐼)((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))(2nd ‘𝐼) ↔ ((1st ‘𝐼)(𝐶 Func 𝐶)(2nd ‘𝐼) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘𝐼)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1-onto→(((1st ‘𝐼)‘𝑥)(Hom ‘𝐶)((1st ‘𝐼)‘𝑦)))) | 
| 24 | 8, 22, 23 | sylanbrc 583 | . . 3
⊢ (𝐶 ∈ Cat →
(1st ‘𝐼)((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))(2nd ‘𝐼)) | 
| 25 |  | df-br 5144 | . . 3
⊢
((1st ‘𝐼)((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))(2nd ‘𝐼) ↔ 〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | 
| 26 | 24, 25 | sylib 218 | . 2
⊢ (𝐶 ∈ Cat →
〈(1st ‘𝐼), (2nd ‘𝐼)〉 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) | 
| 27 | 5, 26 | eqeltrd 2841 | 1
⊢ (𝐶 ∈ Cat → 𝐼 ∈ ((𝐶 Full 𝐶) ∩ (𝐶 Faith 𝐶))) |