| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | relfunc 17907 | . . 3
⊢ Rel
(𝐶 Func 𝐸) | 
| 2 |  | fthfunc 17954 | . . . . 5
⊢ (𝐶 Faith 𝐷) ⊆ (𝐶 Func 𝐷) | 
| 3 |  | cofth.f | . . . . 5
⊢ (𝜑 → 𝐹 ∈ (𝐶 Faith 𝐷)) | 
| 4 | 2, 3 | sselid 3981 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷)) | 
| 5 |  | fthfunc 17954 | . . . . 5
⊢ (𝐷 Faith 𝐸) ⊆ (𝐷 Func 𝐸) | 
| 6 |  | cofth.g | . . . . 5
⊢ (𝜑 → 𝐺 ∈ (𝐷 Faith 𝐸)) | 
| 7 | 5, 6 | sselid 3981 | . . . 4
⊢ (𝜑 → 𝐺 ∈ (𝐷 Func 𝐸)) | 
| 8 | 4, 7 | cofucl 17933 | . . 3
⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) | 
| 9 |  | 1st2nd 8064 | . . 3
⊢ ((Rel
(𝐶 Func 𝐸) ∧ (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) → (𝐺 ∘func 𝐹) = 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉) | 
| 10 | 1, 8, 9 | sylancr 587 | . 2
⊢ (𝜑 → (𝐺 ∘func 𝐹) = 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉) | 
| 11 |  | 1st2ndbr 8067 | . . . . 5
⊢ ((Rel
(𝐶 Func 𝐸) ∧ (𝐺 ∘func 𝐹) ∈ (𝐶 Func 𝐸)) → (1st ‘(𝐺 ∘func
𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) | 
| 12 | 1, 8, 11 | sylancr 587 | . . . 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 |  | relfth 17956 | . . . . . . . . 9
⊢ Rel
(𝐷 Faith 𝐸) | 
| 17 | 6 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Faith 𝐸)) | 
| 18 |  | 1st2ndbr 8067 | . . . . . . . . 9
⊢ ((Rel
(𝐷 Faith 𝐸) ∧ 𝐺 ∈ (𝐷 Faith 𝐸)) → (1st ‘𝐺)(𝐷 Faith 𝐸)(2nd ‘𝐺)) | 
| 19 | 16, 17, 18 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐺)(𝐷 Faith 𝐸)(2nd ‘𝐺)) | 
| 20 |  | eqid 2737 | . . . . . . . . . 10
⊢
(Base‘𝐶) =
(Base‘𝐶) | 
| 21 |  | relfunc 17907 | . . . . . . . . . . 11
⊢ Rel
(𝐶 Func 𝐷) | 
| 22 | 4 | adantr 480 | . . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Func 𝐷)) | 
| 23 |  | 1st2ndbr 8067 | . . . . . . . . . . 11
⊢ ((Rel
(𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 24 | 21, 22, 23 | sylancr 587 | . . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹)) | 
| 25 | 20, 13, 24 | funcf1 17911 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹):(Base‘𝐶)⟶(Base‘𝐷)) | 
| 26 |  | simprl 771 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑥 ∈ (Base‘𝐶)) | 
| 27 | 25, 26 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑥) ∈ (Base‘𝐷)) | 
| 28 |  | simprr 773 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝑦 ∈ (Base‘𝐶)) | 
| 29 | 25, 28 | ffvelcdmd 7105 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘𝐹)‘𝑦) ∈ (Base‘𝐷)) | 
| 30 | 13, 14, 15, 19, 27, 29 | fthf1 17964 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))–1-1→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) | 
| 31 |  | eqid 2737 | . . . . . . . 8
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) | 
| 32 |  | relfth 17956 | . . . . . . . . 9
⊢ Rel
(𝐶 Faith 𝐷) | 
| 33 | 3 | adantr 480 | . . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐹 ∈ (𝐶 Faith 𝐷)) | 
| 34 |  | 1st2ndbr 8067 | . . . . . . . . 9
⊢ ((Rel
(𝐶 Faith 𝐷) ∧ 𝐹 ∈ (𝐶 Faith 𝐷)) → (1st ‘𝐹)(𝐶 Faith 𝐷)(2nd ‘𝐹)) | 
| 35 | 32, 33, 34 | sylancr 587 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (1st ‘𝐹)(𝐶 Faith 𝐷)(2nd ‘𝐹)) | 
| 36 | 20, 31, 14, 35, 26, 28 | fthf1 17964 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) | 
| 37 |  | f1co 6815 | . . . . . . 7
⊢
(((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))–1-1→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))) ∧ (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘𝐹)‘𝑥)(Hom ‘𝐷)((1st ‘𝐹)‘𝑦))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) | 
| 38 | 30, 36, 37 | syl2anc 584 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) | 
| 39 | 7 | adantr 480 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → 𝐺 ∈ (𝐷 Func 𝐸)) | 
| 40 | 20, 22, 39, 26, 28 | cofu2nd 17930 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) | 
| 41 |  | eqidd 2738 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(Hom ‘𝐶)𝑦) = (𝑥(Hom ‘𝐶)𝑦)) | 
| 42 | 20, 22, 39, 26 | cofu1 17929 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑥) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑥))) | 
| 43 | 20, 22, 39, 28 | cofu1 17929 | . . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((1st ‘(𝐺 ∘func
𝐹))‘𝑦) = ((1st
‘𝐺)‘((1st ‘𝐹)‘𝑦))) | 
| 44 | 42, 43 | oveq12d 7449 | . . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (((1st ‘(𝐺 ∘func
𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) = (((1st ‘𝐺)‘((1st
‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦)))) | 
| 45 | 40, 41, 44 | f1eq123d 6840 | . . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → ((𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)) ↔ ((((1st ‘𝐹)‘𝑥)(2nd ‘𝐺)((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘𝐺)‘((1st ‘𝐹)‘𝑥))(Hom ‘𝐸)((1st ‘𝐺)‘((1st ‘𝐹)‘𝑦))))) | 
| 46 | 38, 45 | mpbird 257 | . . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (Base‘𝐶) ∧ 𝑦 ∈ (Base‘𝐶))) → (𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦))) | 
| 47 | 46 | ralrimivva 3202 | . . . 4
⊢ (𝜑 → ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦))) | 
| 48 | 20, 31, 15 | isfth2 17962 | . . . 4
⊢
((1st ‘(𝐺 ∘func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ ((1st
‘(𝐺
∘func 𝐹))(𝐶 Func 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ∧ ∀𝑥 ∈ (Base‘𝐶)∀𝑦 ∈ (Base‘𝐶)(𝑥(2nd ‘(𝐺 ∘func 𝐹))𝑦):(𝑥(Hom ‘𝐶)𝑦)–1-1→(((1st ‘(𝐺 ∘func 𝐹))‘𝑥)(Hom ‘𝐸)((1st ‘(𝐺 ∘func 𝐹))‘𝑦)))) | 
| 49 | 12, 47, 48 | sylanbrc 583 | . . 3
⊢ (𝜑 → (1st
‘(𝐺
∘func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺 ∘func 𝐹))) | 
| 50 |  | df-br 5144 | . . 3
⊢
((1st ‘(𝐺 ∘func 𝐹))(𝐶 Faith 𝐸)(2nd ‘(𝐺 ∘func 𝐹)) ↔ 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Faith 𝐸)) | 
| 51 | 49, 50 | sylib 218 | . 2
⊢ (𝜑 → 〈(1st
‘(𝐺
∘func 𝐹)), (2nd ‘(𝐺 ∘func
𝐹))〉 ∈ (𝐶 Faith 𝐸)) | 
| 52 | 10, 51 | eqeltrd 2841 | 1
⊢ (𝜑 → (𝐺 ∘func 𝐹) ∈ (𝐶 Faith 𝐸)) |