Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  catciso Structured version   Visualization version   GIF version

Theorem catciso 17359
 Description: A functor is an isomorphism of categories if and only if it is full and faithful, and is a bijection on the objects. Remark 3.28(2) in [Adamek] p. 34. (Contributed by Mario Carneiro, 29-Jan-2017.)
Hypotheses
Ref Expression
catciso.c 𝐶 = (CatCat‘𝑈)
catciso.b 𝐵 = (Base‘𝐶)
catciso.r 𝑅 = (Base‘𝑋)
catciso.s 𝑆 = (Base‘𝑌)
catciso.u (𝜑𝑈𝑉)
catciso.x (𝜑𝑋𝐵)
catciso.y (𝜑𝑌𝐵)
catciso.i 𝐼 = (Iso‘𝐶)
Assertion
Ref Expression
catciso (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)))

Proof of Theorem catciso
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 relfunc 17124 . . . . 5 Rel (𝑋 Func 𝑌)
2 catciso.b . . . . . . . . . . . . . 14 𝐵 = (Base‘𝐶)
3 eqid 2819 . . . . . . . . . . . . . 14 (Inv‘𝐶) = (Inv‘𝐶)
4 catciso.u . . . . . . . . . . . . . . 15 (𝜑𝑈𝑉)
5 catciso.c . . . . . . . . . . . . . . . 16 𝐶 = (CatCat‘𝑈)
65catccat 17356 . . . . . . . . . . . . . . 15 (𝑈𝑉𝐶 ∈ Cat)
74, 6syl 17 . . . . . . . . . . . . . 14 (𝜑𝐶 ∈ Cat)
8 catciso.x . . . . . . . . . . . . . 14 (𝜑𝑋𝐵)
9 catciso.y . . . . . . . . . . . . . 14 (𝜑𝑌𝐵)
10 catciso.i . . . . . . . . . . . . . 14 𝐼 = (Iso‘𝐶)
112, 3, 7, 8, 9, 10isoval 17027 . . . . . . . . . . . . 13 (𝜑 → (𝑋𝐼𝑌) = dom (𝑋(Inv‘𝐶)𝑌))
1211eleq2d 2896 . . . . . . . . . . . 12 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌)))
1312biimpa 479 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌))
147adantr 483 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐶 ∈ Cat)
158adantr 483 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝑋𝐵)
169adantr 483 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝑌𝐵)
172, 3, 14, 15, 16invfun 17026 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → Fun (𝑋(Inv‘𝐶)𝑌))
18 funfvbrb 6814 . . . . . . . . . . . 12 (Fun (𝑋(Inv‘𝐶)𝑌) → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
1917, 18syl 17 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ dom (𝑋(Inv‘𝐶)𝑌) ↔ 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
2013, 19mpbid 234 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))
21 eqid 2819 . . . . . . . . . . 11 (Sect‘𝐶) = (Sect‘𝐶)
222, 3, 14, 15, 16, 21isinv 17022 . . . . . . . . . 10 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Inv‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ↔ (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)))
2320, 22mpbid 234 . . . . . . . . 9 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹))
2423simpld 497 . . . . . . . 8 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹))
25 eqid 2819 . . . . . . . . 9 (Hom ‘𝐶) = (Hom ‘𝐶)
26 eqid 2819 . . . . . . . . 9 (comp‘𝐶) = (comp‘𝐶)
27 eqid 2819 . . . . . . . . 9 (Id‘𝐶) = (Id‘𝐶)
282, 25, 26, 27, 21, 14, 15, 16issect 17015 . . . . . . . 8 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(𝑋(Sect‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹) ↔ (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))))
2924, 28mpbid 234 . . . . . . 7 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋)))
3029simp1d 1136 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌))
315, 2, 4, 25, 8, 9catchom 17351 . . . . . . 7 (𝜑 → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
3231adantr 483 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝑋(Hom ‘𝐶)𝑌) = (𝑋 Func 𝑌))
3330, 32eleqtrd 2913 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ (𝑋 Func 𝑌))
34 1st2nd 7730 . . . . 5 ((Rel (𝑋 Func 𝑌) ∧ 𝐹 ∈ (𝑋 Func 𝑌)) → 𝐹 = ⟨(1st𝐹), (2nd𝐹)⟩)
351, 33, 34sylancr 589 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 = ⟨(1st𝐹), (2nd𝐹)⟩)
36 1st2ndbr 7733 . . . . . . 7 ((Rel (𝑋 Func 𝑌) ∧ 𝐹 ∈ (𝑋 Func 𝑌)) → (1st𝐹)(𝑋 Func 𝑌)(2nd𝐹))
371, 33, 36sylancr 589 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st𝐹)(𝑋 Func 𝑌)(2nd𝐹))
38 catciso.r . . . . . . . . 9 𝑅 = (Base‘𝑋)
39 eqid 2819 . . . . . . . . 9 (Hom ‘𝑋) = (Hom ‘𝑋)
40 eqid 2819 . . . . . . . . 9 (Hom ‘𝑌) = (Hom ‘𝑌)
4137adantr 483 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (1st𝐹)(𝑋 Func 𝑌)(2nd𝐹))
42 simprl 769 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝑥𝑅)
43 simprr 771 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝑦𝑅)
4438, 39, 40, 41, 42, 43funcf2 17130 . . . . . . . 8 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)⟶(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦)))
45 catciso.s . . . . . . . . . 10 𝑆 = (Base‘𝑌)
46 relfunc 17124 . . . . . . . . . . . 12 Rel (𝑌 Func 𝑋)
4729simp2d 1137 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋))
485, 2, 4, 25, 9, 8catchom 17351 . . . . . . . . . . . . . 14 (𝜑 → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
4948adantr 483 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝑌(Hom ‘𝐶)𝑋) = (𝑌 Func 𝑋))
5047, 49eleqtrd 2913 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋))
51 1st2ndbr 7733 . . . . . . . . . . . 12 ((Rel (𝑌 Func 𝑋) ∧ ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
5246, 50, 51sylancr 589 . . . . . . . . . . 11 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
5352adantr 483 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))(𝑌 Func 𝑋)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
5438, 45, 41funcf1 17128 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (1st𝐹):𝑅𝑆)
5554, 42ffvelrnd 6845 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st𝐹)‘𝑥) ∈ 𝑆)
5654, 43ffvelrnd 6845 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st𝐹)‘𝑦) ∈ 𝑆)
5745, 40, 39, 53, 55, 56funcf2 17130 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))⟶(((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))))
5829simp3d 1138 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = ((Id‘𝐶)‘𝑋))
594adantr 483 . . . . . . . . . . . . . . . . 17 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝑈𝑉)
605, 2, 59, 26, 15, 16, 15, 33, 50catcco 17353 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(⟨𝑋, 𝑌⟩(comp‘𝐶)𝑋)𝐹) = (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))
61 eqid 2819 . . . . . . . . . . . . . . . . . 18 (idfunc𝑋) = (idfunc𝑋)
625, 2, 27, 61, 4, 8catcid 17355 . . . . . . . . . . . . . . . . 17 (𝜑 → ((Id‘𝐶)‘𝑋) = (idfunc𝑋))
6362adantr 483 . . . . . . . . . . . . . . . 16 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((Id‘𝐶)‘𝑋) = (idfunc𝑋))
6458, 60, 633eqtr3d 2862 . . . . . . . . . . . . . . 15 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹) = (idfunc𝑋))
6564adantr 483 . . . . . . . . . . . . . 14 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹) = (idfunc𝑋))
6665fveq2d 6667 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (1st ‘(idfunc𝑋)))
6766fveq1d 6665 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑥) = ((1st ‘(idfunc𝑋))‘𝑥))
6833adantr 483 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝐹 ∈ (𝑋 Func 𝑌))
6950adantr 483 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌 Func 𝑋))
7038, 68, 69, 42cofu1 17146 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑥) = ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥)))
715, 2, 4catcbas 17349 . . . . . . . . . . . . . . . 16 (𝜑𝐵 = (𝑈 ∩ Cat))
72 inss2 4204 . . . . . . . . . . . . . . . 16 (𝑈 ∩ Cat) ⊆ Cat
7371, 72eqsstrdi 4019 . . . . . . . . . . . . . . 15 (𝜑𝐵 ⊆ Cat)
7473, 8sseldd 3966 . . . . . . . . . . . . . 14 (𝜑𝑋 ∈ Cat)
7574ad2antrr 724 . . . . . . . . . . . . 13 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝑋 ∈ Cat)
7661, 38, 75, 42idfu1 17142 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(idfunc𝑋))‘𝑥) = 𝑥)
7767, 70, 763eqtr3d 2862 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥)) = 𝑥)
7866fveq1d 6665 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑦) = ((1st ‘(idfunc𝑋))‘𝑦))
7938, 68, 69, 43cofu1 17146 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))‘𝑦) = ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦)))
8061, 38, 75, 43idfu1 17142 . . . . . . . . . . . 12 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘(idfunc𝑋))‘𝑦) = 𝑦)
8178, 79, 803eqtr3d 2862 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦)) = 𝑦)
8277, 81oveq12d 7166 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))) = (𝑥(Hom ‘𝑋)𝑦))
8382feq3d 6494 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))⟶(((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(Hom ‘𝑋)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))) ↔ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))⟶(𝑥(Hom ‘𝑋)𝑦)))
8457, 83mpbid 234 . . . . . . . 8 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)):(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))⟶(𝑥(Hom ‘𝑋)𝑦))
8565fveq2d 6667 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (2nd ‘(idfunc𝑋)))
8685oveqd 7165 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))𝑦) = (𝑥(2nd ‘(idfunc𝑋))𝑦))
8738, 68, 69, 42, 43cofu2nd 17147 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(2nd ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹))𝑦) = ((((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)))
8861, 38, 75, 39, 42, 43idfu2nd 17139 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(2nd ‘(idfunc𝑋))𝑦) = ( I ↾ (𝑥(Hom ‘𝑋)𝑦)))
8986, 87, 883eqtr3d 2862 . . . . . . . 8 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦)) ∘ (𝑥(2nd𝐹)𝑦)) = ( I ↾ (𝑥(Hom ‘𝑋)𝑦)))
9023simprd 498 . . . . . . . . . . . . . . 15 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹)
912, 25, 26, 27, 21, 14, 16, 15issect 17015 . . . . . . . . . . . . . . 15 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹)(𝑌(Sect‘𝐶)𝑋)𝐹 ↔ (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌))))
9290, 91mpbid 234 . . . . . . . . . . . . . 14 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∈ (𝑌(Hom ‘𝐶)𝑋) ∧ 𝐹 ∈ (𝑋(Hom ‘𝐶)𝑌) ∧ (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌)))
9392simp3d 1138 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = ((Id‘𝐶)‘𝑌))
945, 2, 59, 26, 16, 15, 16, 50, 33catcco 17353 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹(⟨𝑌, 𝑋⟩(comp‘𝐶)𝑌)((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))
95 eqid 2819 . . . . . . . . . . . . . . 15 (idfunc𝑌) = (idfunc𝑌)
965, 2, 27, 95, 4, 9catcid 17355 . . . . . . . . . . . . . 14 (𝜑 → ((Id‘𝐶)‘𝑌) = (idfunc𝑌))
9796adantr 483 . . . . . . . . . . . . 13 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((Id‘𝐶)‘𝑌) = (idfunc𝑌))
9893, 94, 973eqtr3d 2862 . . . . . . . . . . . 12 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (idfunc𝑌))
9998adantr 483 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)) = (idfunc𝑌))
10099fveq2d 6667 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (2nd ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = (2nd ‘(idfunc𝑌)))
101100oveqd 7165 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st𝐹)‘𝑦)) = (((1st𝐹)‘𝑥)(2nd ‘(idfunc𝑌))((1st𝐹)‘𝑦)))
10245, 69, 68, 55, 56cofu2nd 17147 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st𝐹)‘𝑦)) = ((((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(2nd𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))) ∘ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦))))
10377, 81oveq12d 7166 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(2nd𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))) = (𝑥(2nd𝐹)𝑦))
104103coeq1d 5725 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑥))(2nd𝐹)((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))‘((1st𝐹)‘𝑦))) ∘ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦))) = ((𝑥(2nd𝐹)𝑦) ∘ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦))))
105102, 104eqtrd 2854 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹)))((1st𝐹)‘𝑦)) = ((𝑥(2nd𝐹)𝑦) ∘ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦))))
10673ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝐵 ⊆ Cat)
1079ad2antrr 724 . . . . . . . . . . 11 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝑌𝐵)
108106, 107sseldd 3966 . . . . . . . . . 10 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → 𝑌 ∈ Cat)
10995, 45, 108, 40, 55, 56idfu2nd 17139 . . . . . . . . 9 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (((1st𝐹)‘𝑥)(2nd ‘(idfunc𝑌))((1st𝐹)‘𝑦)) = ( I ↾ (((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))))
110101, 105, 1093eqtr3d 2862 . . . . . . . 8 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → ((𝑥(2nd𝐹)𝑦) ∘ (((1st𝐹)‘𝑥)(2nd ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))((1st𝐹)‘𝑦))) = ( I ↾ (((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))))
11144, 84, 89, 110fcof1od 7042 . . . . . . 7 (((𝜑𝐹 ∈ (𝑋𝐼𝑌)) ∧ (𝑥𝑅𝑦𝑅)) → (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦)))
112111ralrimivva 3189 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ∀𝑥𝑅𝑦𝑅 (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦)))
11338, 39, 40isffth2 17178 . . . . . 6 ((1st𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd𝐹) ↔ ((1st𝐹)(𝑋 Func 𝑌)(2nd𝐹) ∧ ∀𝑥𝑅𝑦𝑅 (𝑥(2nd𝐹)𝑦):(𝑥(Hom ‘𝑋)𝑦)–1-1-onto→(((1st𝐹)‘𝑥)(Hom ‘𝑌)((1st𝐹)‘𝑦))))
11437, 112, 113sylanbrc 585 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd𝐹))
115 df-br 5058 . . . . 5 ((1st𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd𝐹) ↔ ⟨(1st𝐹), (2nd𝐹)⟩ ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)))
116114, 115sylib 220 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ⟨(1st𝐹), (2nd𝐹)⟩ ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)))
11735, 116eqeltrd 2911 . . 3 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)))
11838, 45, 37funcf1 17128 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st𝐹):𝑅𝑆)
11945, 38, 52funcf1 17128 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)):𝑆𝑅)
12064fveq2d 6667 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = (1st ‘(idfunc𝑋)))
12138, 33, 50cofu1st 17145 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(((𝑋(Inv‘𝐶)𝑌)‘𝐹) ∘func 𝐹)) = ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∘ (1st𝐹)))
12274adantr 483 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝑋 ∈ Cat)
12361, 38, 122idfu1st 17141 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(idfunc𝑋)) = ( I ↾ 𝑅))
124120, 121, 1233eqtr3d 2862 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹)) ∘ (1st𝐹)) = ( I ↾ 𝑅))
12598fveq2d 6667 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = (1st ‘(idfunc𝑌)))
12645, 50, 33cofu1st 17145 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(𝐹func ((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = ((1st𝐹) ∘ (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))))
12773, 9sseldd 3966 . . . . . . 7 (𝜑𝑌 ∈ Cat)
128127adantr 483 . . . . . 6 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → 𝑌 ∈ Cat)
12995, 45, 128idfu1st 17141 . . . . 5 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st ‘(idfunc𝑌)) = ( I ↾ 𝑆))
130125, 126, 1293eqtr3d 2862 . . . 4 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → ((1st𝐹) ∘ (1st ‘((𝑋(Inv‘𝐶)𝑌)‘𝐹))) = ( I ↾ 𝑆))
131118, 119, 124, 130fcof1od 7042 . . 3 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (1st𝐹):𝑅1-1-onto𝑆)
132117, 131jca 514 . 2 ((𝜑𝐹 ∈ (𝑋𝐼𝑌)) → (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆))
1337adantr 483 . . 3 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐶 ∈ Cat)
1348adantr 483 . . 3 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝑋𝐵)
1359adantr 483 . . 3 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝑌𝐵)
136 inss1 4203 . . . . . . 7 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Full 𝑌)
137 fullfunc 17168 . . . . . . 7 (𝑋 Full 𝑌) ⊆ (𝑋 Func 𝑌)
138136, 137sstri 3974 . . . . . 6 ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ⊆ (𝑋 Func 𝑌)
139 simprl 769 . . . . . 6 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)))
140138, 139sseldi 3963 . . . . 5 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐹 ∈ (𝑋 Func 𝑌))
1411, 140, 34sylancr 589 . . . 4 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐹 = ⟨(1st𝐹), (2nd𝐹)⟩)
1424adantr 483 . . . . 5 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝑈𝑉)
143 eqid 2819 . . . . 5 (𝑥𝑆, 𝑦𝑆(((1st𝐹)‘𝑥)(2nd𝐹)((1st𝐹)‘𝑦))) = (𝑥𝑆, 𝑦𝑆(((1st𝐹)‘𝑥)(2nd𝐹)((1st𝐹)‘𝑦)))
144141, 139eqeltrrd 2912 . . . . . 6 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → ⟨(1st𝐹), (2nd𝐹)⟩ ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)))
145144, 115sylibr 236 . . . . 5 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → (1st𝐹)((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌))(2nd𝐹))
146 simprr 771 . . . . 5 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → (1st𝐹):𝑅1-1-onto𝑆)
1475, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146catcisolem 17358 . . . 4 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → ⟨(1st𝐹), (2nd𝐹)⟩(𝑋(Inv‘𝐶)𝑌)⟨(1st𝐹), (𝑥𝑆, 𝑦𝑆(((1st𝐹)‘𝑥)(2nd𝐹)((1st𝐹)‘𝑦)))⟩)
148141, 147eqbrtrd 5079 . . 3 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐹(𝑋(Inv‘𝐶)𝑌)⟨(1st𝐹), (𝑥𝑆, 𝑦𝑆(((1st𝐹)‘𝑥)(2nd𝐹)((1st𝐹)‘𝑦)))⟩)
1492, 3, 133, 134, 135, 10, 148inviso1 17028 . 2 ((𝜑 ∧ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)) → 𝐹 ∈ (𝑋𝐼𝑌))
150132, 149impbida 799 1 (𝜑 → (𝐹 ∈ (𝑋𝐼𝑌) ↔ (𝐹 ∈ ((𝑋 Full 𝑌) ∩ (𝑋 Faith 𝑌)) ∧ (1st𝐹):𝑅1-1-onto𝑆)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 398   ∧ w3a 1081   = wceq 1530   ∈ wcel 2107  ∀wral 3136   ∩ cin 3933   ⊆ wss 3934  ⟨cop 4565   class class class wbr 5057   I cid 5452  ◡ccnv 5547  dom cdm 5548   ↾ cres 5550   ∘ ccom 5552  Rel wrel 5553  Fun wfun 6342  ⟶wf 6344  –1-1-onto→wf1o 6347  ‘cfv 6348  (class class class)co 7148   ∈ cmpo 7150  1st c1st 7679  2nd c2nd 7680  Basecbs 16475  Hom chom 16568  compcco 16569  Catccat 16927  Idccid 16928  Sectcsect 17006  Invcinv 17007  Isociso 17008   Func cfunc 17116  idfunccidfu 17117   ∘func ccofu 17118   Full cful 17164   Faith cfth 17165  CatCatccatc 17346 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791  ax-rep 5181  ax-sep 5194  ax-nul 5201  ax-pow 5257  ax-pr 5320  ax-un 7453  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2616  df-eu 2648  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-ne 3015  df-nel 3122  df-ral 3141  df-rex 3142  df-reu 3143  df-rmo 3144  df-rab 3145  df-v 3495  df-sbc 3771  df-csb 3882  df-dif 3937  df-un 3939  df-in 3941  df-ss 3950  df-pss 3952  df-nul 4290  df-if 4466  df-pw 4539  df-sn 4560  df-pr 4562  df-tp 4564  df-op 4566  df-uni 4831  df-int 4868  df-iun 4912  df-br 5058  df-opab 5120  df-mpt 5138  df-tr 5164  df-id 5453  df-eprel 5458  df-po 5467  df-so 5468  df-fr 5507  df-we 5509  df-xp 5554  df-rel 5555  df-cnv 5556  df-co 5557  df-dm 5558  df-rn 5559  df-res 5560  df-ima 5561  df-pred 6141  df-ord 6187  df-on 6188  df-lim 6189  df-suc 6190  df-iota 6307  df-fun 6350  df-fn 6351  df-f 6352  df-f1 6353  df-fo 6354  df-f1o 6355  df-fv 6356  df-riota 7106  df-ov 7151  df-oprab 7152  df-mpo 7153  df-om 7573  df-1st 7681  df-2nd 7682  df-wrecs 7939  df-recs 8000  df-rdg 8038  df-1o 8094  df-oadd 8098  df-er 8281  df-map 8400  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-fz 12885  df-struct 16477  df-ndx 16478  df-slot 16479  df-base 16481  df-hom 16581  df-cco 16582  df-cat 16931  df-cid 16932  df-sect 17009  df-inv 17010  df-iso 17011  df-func 17120  df-idfu 17121  df-cofu 17122  df-full 17166  df-fth 17167  df-catc 17347 This theorem is referenced by:  yoniso  17527
 Copyright terms: Public domain W3C validator