Step | Hyp | Ref
| Expression |
1 | | relfunc 17577 |
. . . . 5
⊢ Rel
(𝑋 Func 𝑌) |
2 | | catciso.b |
. . . . . . . . . . . . . 14
⊢ 𝐵 = (Base‘𝐶) |
3 | | eqid 2738 |
. . . . . . . . . . . . . 14
⊢
(Inv‘𝐶) =
(Inv‘𝐶) |
4 | | catciso.u |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑈 ∈ 𝑉) |
5 | | catciso.c |
. . . . . . . . . . . . . . . 16
⊢ 𝐶 = (CatCat‘𝑈) |
6 | 5 | catccat 17823 |
. . . . . . . . . . . . . . 15
⊢ (𝑈 ∈ 𝑉 → 𝐶 ∈ Cat) |
7 | 4, 6 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐶 ∈ Cat) |
8 | | catciso.x |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ 𝐵) |
9 | | catciso.y |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑌 ∈ 𝐵) |
10 | | catciso.i |
. . . . . . . . . . . . . 14
⊢ 𝐼 = (Iso‘𝐶) |
11 | 2, 3, 7, 8, 9, 10 | isoval 17477 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝑋𝐼𝑌) = dom (𝑋(Inv‘𝐶)𝑌)) |
12 | 11 | eleq2d 2824 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌))) |
13 | 12 | biimpa 477 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)) |
14 | 7 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ Cat) |
15 | 8 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ 𝐵) |
16 | 9 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ 𝐵) |
17 | 2, 3, 14, 15, 16 | invfun 17476 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → Fun (𝑋(Inv‘𝐶)𝑌)) |
18 | | funfvbrb 6928 |
. . . . . . . . . . . 12
⊢ (Fun
(𝑋(Inv‘𝐶)𝑌) → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
20 | 13, 19 | mpbid 231 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) |
21 | | eqid 2738 |
. . . . . . . . . . 11
⊢
(Sect‘𝐶) =
(Sect‘𝐶) |
22 | 2, 3, 14, 15, 16, 21 | isinv 17472 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹))) |
23 | 20, 22 | mpbid 231 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)) |
24 | 23 | simpld 495 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) |
25 | | eqid 2738 |
. . . . . . . . 9
⊢ (Hom
‘𝐶) = (Hom
‘𝐶) |
26 | | eqid 2738 |
. . . . . . . . 9
⊢
(comp‘𝐶) =
(comp‘𝐶) |
27 | | eqid 2738 |
. . . . . . . . 9
⊢
(Id‘𝐶) =
(Id‘𝐶) |
28 | 2, 25, 26, 27, 21, 14, 15, 16 | issect 17465 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))) |
29 | 24, 28 | mpbid 231 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))) |
30 | 29 | simp1d 1141 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌)) |
31 | 5, 2, 4, 25, 8, 9 | catchom 17818 |
. . . . . . 7
⊢ (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌)) |
32 | 31 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌)) |
33 | 30, 32 | eleqtrd 2841 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ (𝑋 Func 𝑌)) |
34 | | 1st2nd 7880 |
. . . . 5
⊢ ((Rel
(𝑋 Func 𝑌) ∧ 𝐹 ∈ (𝑋 Func 𝑌)) → 𝐹 = 〈(1st ‘𝐹), (2nd ‘𝐹)〉) |
35 | 1, 33, 34 | sylancr 587 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 = 〈(1st ‘𝐹), (2nd ‘𝐹)〉) |
36 | | 1st2ndbr 7883 |
. . . . . . 7
⊢ ((Rel
(𝑋 Func 𝑌) ∧ 𝐹 ∈ (𝑋 Func 𝑌)) → (1st ‘𝐹)(𝑋 Func 𝑌)(2nd ‘𝐹)) |
37 | 1, 33, 36 | sylancr 587 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘𝐹)(𝑋 Func 𝑌)(2nd ‘𝐹)) |
38 | | catciso.r |
. . . . . . . . 9
⊢ 𝑅 = (Base‘𝑋) |
39 | | eqid 2738 |
. . . . . . . . 9
⊢ (Hom
‘𝑋) = (Hom
‘𝑋) |
40 | | eqid 2738 |
. . . . . . . . 9
⊢ (Hom
‘𝑌) = (Hom
‘𝑌) |
41 | 37 | adantr 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (1st ‘𝐹)(𝑋 Func 𝑌)(2nd ‘𝐹)) |
42 | | simprl 768 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑥 ∈ 𝑅) |
43 | | simprr 770 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑦 ∈ 𝑅) |
44 | 38, 39, 40, 41, 42, 43 | funcf2 17583 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)⟶(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))) |
45 | | catciso.s |
. . . . . . . . . 10
⊢ 𝑆 = (Base‘𝑌) |
46 | | relfunc 17577 |
. . . . . . . . . . . 12
⊢ Rel
(𝑌 Func 𝑋) |
47 | 29 | simp2d 1142 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋)) |
48 | 5, 2, 4, 25, 9, 8 | catchom 17818 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋)) |
49 | 48 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋)) |
50 | 47, 49 | eleqtrd 2841 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋)) |
51 | | 1st2ndbr 7883 |
. . . . . . . . . . . 12
⊢ ((Rel
(𝑌 Func 𝑋) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
52 | 46, 50, 51 | sylancr 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
53 | 52 | adantr 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
54 | 38, 45, 41 | funcf1 17581 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (1st ‘𝐹):𝑅⟶𝑆) |
55 | 54, 42 | ffvelrnd 6962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘𝐹)‘𝑥) ∈ 𝑆) |
56 | 54, 43 | ffvelrnd 6962 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘𝐹)‘𝑦) ∈ 𝑆) |
57 | 45, 40, 39, 53, 55, 56 | funcf2 17583 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))⟶(((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦)))) |
58 | 29 | simp3d 1143 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)) |
59 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝑈 ∈ 𝑉) |
60 | 5, 2, 59, 26, 15, 16, 15, 33, 50 | catcco 17820 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(〈𝑋, 𝑌〉(comp‘𝐶)𝑋)𝐹) = (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) |
61 | | eqid 2738 |
. . . . . . . . . . . . . . . . . 18
⊢
(idfunc‘𝑋) = (idfunc‘𝑋) |
62 | 5, 2, 27, 61, 4, 8 | catcid 17822 |
. . . . . . . . . . . . . . . . 17
⊢ (𝜑 → ((Id‘𝐶)‘𝑋) = (idfunc‘𝑋)) |
63 | 62 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((Id‘𝐶)‘𝑋) = (idfunc‘𝑋)) |
64 | 58, 60, 63 | 3eqtr3d 2786 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹) =
(idfunc‘𝑋)) |
65 | 64 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹) =
(idfunc‘𝑋)) |
66 | 65 | fveq2d 6778 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (1st
‘(idfunc‘𝑋))) |
67 | 66 | fveq1d 6776 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑥) = ((1st
‘(idfunc‘𝑋))‘𝑥)) |
68 | 33 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝐹 ∈ (𝑋 Func 𝑌)) |
69 | 50 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋)) |
70 | 38, 68, 69, 42 | cofu1 17599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑥) = ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))) |
71 | 5, 2, 4 | catcbas 17816 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝐵 = (𝑈 ∩ Cat)) |
72 | | inss2 4163 |
. . . . . . . . . . . . . . . 16
⊢ (𝑈 ∩ Cat) ⊆
Cat |
73 | 71, 72 | eqsstrdi 3975 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐵 ⊆ Cat) |
74 | 73, 8 | sseldd 3922 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑋 ∈ Cat) |
75 | 74 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑋 ∈ Cat) |
76 | 61, 38, 75, 42 | idfu1 17595 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st
‘(idfunc‘𝑋))‘𝑥) = 𝑥) |
77 | 67, 70, 76 | 3eqtr3d 2786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥)) = 𝑥) |
78 | 66 | fveq1d 6776 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑦) = ((1st
‘(idfunc‘𝑋))‘𝑦)) |
79 | 38, 68, 69, 43 | cofu1 17599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑦) = ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) |
80 | 61, 38, 75, 43 | idfu1 17595 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st
‘(idfunc‘𝑋))‘𝑦) = 𝑦) |
81 | 78, 79, 80 | 3eqtr3d 2786 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦)) = 𝑦) |
82 | 77, 81 | oveq12d 7293 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) = (𝑥(Hom ‘𝑋)𝑦)) |
83 | 82 | feq3d 6587 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))⟶(((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) ↔ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))⟶(𝑥(Hom ‘𝑋)𝑦))) |
84 | 57, 83 | mpbid 231 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)):(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))⟶(𝑥(Hom ‘𝑋)𝑦)) |
85 | 65 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (2nd
‘(idfunc‘𝑋))) |
86 | 85 | oveqd 7292 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))𝑦) = (𝑥(2nd
‘(idfunc‘𝑋))𝑦)) |
87 | 38, 68, 69, 42, 43 | cofu2nd 17600 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))𝑦) = ((((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦))) |
88 | 61, 38, 75, 39, 42, 43 | idfu2nd 17592 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(2nd
‘(idfunc‘𝑋))𝑦) = ( I ↾ (𝑥(Hom ‘𝑋)𝑦))) |
89 | 86, 87, 88 | 3eqtr3d 2786 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)) ∘ (𝑥(2nd ‘𝐹)𝑦)) = ( I ↾ (𝑥(Hom ‘𝑋)𝑦))) |
90 | 23 | simprd 496 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹) |
91 | 2, 25, 26, 27, 21, 14, 16, 15 | issect 17465 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹 ↔ (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌)))) |
92 | 90, 91 | mpbid 231 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌))) |
93 | 92 | simp3d 1143 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌)) |
94 | 5, 2, 59, 26, 16, 15, 16, 50, 33 | catcco 17820 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(〈𝑌, 𝑋〉(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹))) |
95 | | eqid 2738 |
. . . . . . . . . . . . . . 15
⊢
(idfunc‘𝑌) = (idfunc‘𝑌) |
96 | 5, 2, 27, 95, 4, 9 | catcid 17822 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → ((Id‘𝐶)‘𝑌) = (idfunc‘𝑌)) |
97 | 96 | adantr 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((Id‘𝐶)‘𝑌) = (idfunc‘𝑌)) |
98 | 93, 94, 97 | 3eqtr3d 2786 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (idfunc‘𝑌)) |
99 | 98 | adantr 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (idfunc‘𝑌)) |
100 | 99 | fveq2d 6778 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (2nd ‘(𝐹 ∘func
((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = (2nd
‘(idfunc‘𝑌))) |
101 | 100 | oveqd 7292 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd ‘(𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st ‘𝐹)‘𝑦)) = (((1st ‘𝐹)‘𝑥)(2nd
‘(idfunc‘𝑌))((1st ‘𝐹)‘𝑦))) |
102 | 45, 69, 68, 55, 56 | cofu2nd 17600 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd ‘(𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st ‘𝐹)‘𝑦)) = ((((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(2nd ‘𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) ∘ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)))) |
103 | 77, 81 | oveq12d 7293 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(2nd ‘𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) = (𝑥(2nd ‘𝐹)𝑦)) |
104 | 103 | coeq1d 5770 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑥))(2nd ‘𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st ‘𝐹)‘𝑦))) ∘ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦))) = ((𝑥(2nd ‘𝐹)𝑦) ∘ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)))) |
105 | 102, 104 | eqtrd 2778 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd ‘(𝐹 ∘func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st ‘𝐹)‘𝑦)) = ((𝑥(2nd ‘𝐹)𝑦) ∘ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦)))) |
106 | 73 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝐵 ⊆ Cat) |
107 | 9 | ad2antrr 723 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑌 ∈ 𝐵) |
108 | 106, 107 | sseldd 3922 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → 𝑌 ∈ Cat) |
109 | 95, 45, 108, 40, 55, 56 | idfu2nd 17592 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (((1st ‘𝐹)‘𝑥)(2nd
‘(idfunc‘𝑌))((1st ‘𝐹)‘𝑦)) = ( I ↾ (((1st
‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦)))) |
110 | 101, 105,
109 | 3eqtr3d 2786 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → ((𝑥(2nd ‘𝐹)𝑦) ∘ (((1st ‘𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st ‘𝐹)‘𝑦))) = ( I ↾ (((1st
‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦)))) |
111 | 44, 84, 89, 110 | fcof1od 7166 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥 ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) → (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))) |
112 | 111 | ralrimivva 3123 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦))) |
113 | 38, 39, 40 | isffth2 17632 |
. . . . . 6
⊢
((1st ‘𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd ‘𝐹) ↔ ((1st ‘𝐹)(𝑋 Func 𝑌)(2nd ‘𝐹) ∧ ∀𝑥 ∈ 𝑅 ∀𝑦 ∈ 𝑅 (𝑥(2nd ‘𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st ‘𝐹)‘𝑥)(Hom ‘𝑌)((1st ‘𝐹)‘𝑦)))) |
114 | 37, 112, 113 | sylanbrc 583 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd ‘𝐹)) |
115 | | df-br 5075 |
. . . . 5
⊢
((1st ‘𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd ‘𝐹) ↔ 〈(1st ‘𝐹), (2nd ‘𝐹)〉 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))) |
116 | 114, 115 | sylib 217 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 〈(1st ‘𝐹), (2nd ‘𝐹)〉 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))) |
117 | 35, 116 | eqeltrd 2839 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))) |
118 | 38, 45, 37 | funcf1 17581 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘𝐹):𝑅⟶𝑆) |
119 | 45, 38, 52 | funcf1 17581 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)):𝑆⟶𝑅) |
120 | 64 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (1st
‘(idfunc‘𝑋))) |
121 | 38, 33, 50 | cofu1st 17598 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = ((1st
‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∘ (1st ‘𝐹))) |
122 | 74 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ Cat) |
123 | 61, 38, 122 | idfu1st 17594 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st
‘(idfunc‘𝑋)) = ( I ↾ 𝑅)) |
124 | 120, 121,
123 | 3eqtr3d 2786 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∘ (1st ‘𝐹)) = ( I ↾ 𝑅)) |
125 | 98 | fveq2d 6778 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(𝐹 ∘func
((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = (1st
‘(idfunc‘𝑌))) |
126 | 45, 50, 33 | cofu1st 17598 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(𝐹 ∘func
((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = ((1st ‘𝐹) ∘ (1st
‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)))) |
127 | 73, 9 | sseldd 3922 |
. . . . . . 7
⊢ (𝜑 → 𝑌 ∈ Cat) |
128 | 127 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ Cat) |
129 | 95, 45, 128 | idfu1st 17594 |
. . . . 5
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st
‘(idfunc‘𝑌)) = ( I ↾ 𝑆)) |
130 | 125, 126,
129 | 3eqtr3d 2786 |
. . . 4
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → ((1st ‘𝐹) ∘ (1st
‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = ( I ↾ 𝑆)) |
131 | 118, 119,
124, 130 | fcof1od 7166 |
. . 3
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘𝐹):𝑅–1-1-onto→𝑆) |
132 | 117, 131 | jca 512 |
. 2
⊢ ((𝜑 ∧ 𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) |
133 | 7 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐶 ∈ Cat) |
134 | 8 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝑋 ∈ 𝐵) |
135 | 9 | adantr 481 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝑌 ∈ 𝐵) |
136 | | inss1 4162 |
. . . . . . 7
⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌) |
137 | | fullfunc 17622 |
. . . . . . 7
⊢ (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌) |
138 | 136, 137 | sstri 3930 |
. . . . . 6
⊢ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌) |
139 | | simprl 768 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))) |
140 | 138, 139 | sselid 3919 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐹 ∈ (𝑋 Func 𝑌)) |
141 | 1, 140, 34 | sylancr 587 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐹 = 〈(1st ‘𝐹), (2nd ‘𝐹)〉) |
142 | 4 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝑈 ∈ 𝑉) |
143 | | eqid 2738 |
. . . . 5
⊢ (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡(1st ‘𝐹)‘𝑥)(2nd ‘𝐹)(◡(1st ‘𝐹)‘𝑦))) = (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡(1st ‘𝐹)‘𝑥)(2nd ‘𝐹)(◡(1st ‘𝐹)‘𝑦))) |
144 | 141, 139 | eqeltrrd 2840 |
. . . . . 6
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 〈(1st
‘𝐹), (2nd
‘𝐹)〉 ∈
((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))) |
145 | 144, 115 | sylibr 233 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → (1st
‘𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd ‘𝐹)) |
146 | | simprr 770 |
. . . . 5
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → (1st
‘𝐹):𝑅–1-1-onto→𝑆) |
147 | 5, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146 | catcisolem 17825 |
. . . 4
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 〈(1st
‘𝐹), (2nd
‘𝐹)〉(𝑋(Inv‘𝐶)𝑌)〈◡(1st ‘𝐹), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡(1st ‘𝐹)‘𝑥)(2nd ‘𝐹)(◡(1st ‘𝐹)‘𝑦)))〉) |
148 | 141, 147 | eqbrtrd 5096 |
. . 3
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐹(𝑋(Inv‘𝐶)𝑌)〈◡(1st ‘𝐹), (𝑥 ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ ◡((◡(1st ‘𝐹)‘𝑥)(2nd ‘𝐹)(◡(1st ‘𝐹)‘𝑦)))〉) |
149 | 2, 3, 133, 134, 135, 10, 148 | inviso1 17478 |
. 2
⊢ ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆)) → 𝐹 ∈ (𝑋𝐼𝑌)) |
150 | 132, 149 | impbida 798 |
1
⊢ (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st ‘𝐹):𝑅–1-1-onto→𝑆))) |