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

Theorem catciso 17932
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 17683 . . . . 5 Rel (𝑋 Func π‘Œ)
2 catciso.b . . . . . . . . . . . . . 14 𝐡 = (Baseβ€˜πΆ)
3 eqid 2738 . . . . . . . . . . . . . 14 (Invβ€˜πΆ) = (Invβ€˜πΆ)
4 catciso.u . . . . . . . . . . . . . . 15 (πœ‘ β†’ π‘ˆ ∈ 𝑉)
5 catciso.c . . . . . . . . . . . . . . . 16 𝐢 = (CatCatβ€˜π‘ˆ)
65catccat 17929 . . . . . . . . . . . . . . 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 17583 . . . . . . . . . . . . 13 (πœ‘ β†’ (π‘‹πΌπ‘Œ) = dom (𝑋(Invβ€˜πΆ)π‘Œ))
1211eleq2d 2824 . . . . . . . . . . . 12 (πœ‘ β†’ (𝐹 ∈ (π‘‹πΌπ‘Œ) ↔ 𝐹 ∈ dom (𝑋(Invβ€˜πΆ)π‘Œ)))
1312biimpa 478 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹 ∈ dom (𝑋(Invβ€˜πΆ)π‘Œ))
147adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐢 ∈ Cat)
158adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝑋 ∈ 𝐡)
169adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ π‘Œ ∈ 𝐡)
172, 3, 14, 15, 16invfun 17582 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ Fun (𝑋(Invβ€˜πΆ)π‘Œ))
18 funfvbrb 6997 . . . . . . . . . . . 12 (Fun (𝑋(Invβ€˜πΆ)π‘Œ) β†’ (𝐹 ∈ dom (𝑋(Invβ€˜πΆ)π‘Œ) ↔ 𝐹(𝑋(Invβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
1917, 18syl 17 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹 ∈ dom (𝑋(Invβ€˜πΆ)π‘Œ) ↔ 𝐹(𝑋(Invβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
2013, 19mpbid 231 . . . . . . . . . 10 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹(𝑋(Invβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))
21 eqid 2738 . . . . . . . . . . 11 (Sectβ€˜πΆ) = (Sectβ€˜πΆ)
222, 3, 14, 15, 16, 21isinv 17578 . . . . . . . . . 10 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹(𝑋(Invβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ↔ (𝐹(𝑋(Sectβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∧ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(π‘Œ(Sectβ€˜πΆ)𝑋)𝐹)))
2320, 22mpbid 231 . . . . . . . . 9 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹(𝑋(Sectβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∧ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(π‘Œ(Sectβ€˜πΆ)𝑋)𝐹))
2423simpld 496 . . . . . . . 8 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹(𝑋(Sectβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))
25 eqid 2738 . . . . . . . . 9 (Hom β€˜πΆ) = (Hom β€˜πΆ)
26 eqid 2738 . . . . . . . . 9 (compβ€˜πΆ) = (compβ€˜πΆ)
27 eqid 2738 . . . . . . . . 9 (Idβ€˜πΆ) = (Idβ€˜πΆ)
282, 25, 26, 27, 21, 14, 15, 16issect 17571 . . . . . . . 8 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹(𝑋(Sectβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ↔ (𝐹 ∈ (𝑋(Hom β€˜πΆ)π‘Œ) ∧ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ(Hom β€˜πΆ)𝑋) ∧ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑋)𝐹) = ((Idβ€˜πΆ)β€˜π‘‹))))
2924, 28mpbid 231 . . . . . . 7 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹 ∈ (𝑋(Hom β€˜πΆ)π‘Œ) ∧ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ(Hom β€˜πΆ)𝑋) ∧ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑋)𝐹) = ((Idβ€˜πΆ)β€˜π‘‹)))
3029simp1d 1143 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹 ∈ (𝑋(Hom β€˜πΆ)π‘Œ))
315, 2, 4, 25, 8, 9catchom 17924 . . . . . . 7 (πœ‘ β†’ (𝑋(Hom β€˜πΆ)π‘Œ) = (𝑋 Func π‘Œ))
3231adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝑋(Hom β€˜πΆ)π‘Œ) = (𝑋 Func π‘Œ))
3330, 32eleqtrd 2841 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹 ∈ (𝑋 Func π‘Œ))
34 1st2nd 7961 . . . . 5 ((Rel (𝑋 Func π‘Œ) ∧ 𝐹 ∈ (𝑋 Func π‘Œ)) β†’ 𝐹 = ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩)
351, 33, 34sylancr 588 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹 = ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩)
36 1st2ndbr 7964 . . . . . . 7 ((Rel (𝑋 Func π‘Œ) ∧ 𝐹 ∈ (𝑋 Func π‘Œ)) β†’ (1st β€˜πΉ)(𝑋 Func π‘Œ)(2nd β€˜πΉ))
371, 33, 36sylancr 588 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜πΉ)(𝑋 Func π‘Œ)(2nd β€˜πΉ))
38 catciso.r . . . . . . . . 9 𝑅 = (Baseβ€˜π‘‹)
39 eqid 2738 . . . . . . . . 9 (Hom β€˜π‘‹) = (Hom β€˜π‘‹)
40 eqid 2738 . . . . . . . . 9 (Hom β€˜π‘Œ) = (Hom β€˜π‘Œ)
4137adantr 482 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (1st β€˜πΉ)(𝑋 Func π‘Œ)(2nd β€˜πΉ))
42 simprl 770 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ π‘₯ ∈ 𝑅)
43 simprr 772 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝑦 ∈ 𝑅)
4438, 39, 40, 41, 42, 43funcf2 17689 . . . . . . . 8 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(2nd β€˜πΉ)𝑦):(π‘₯(Hom β€˜π‘‹)𝑦)⟢(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦)))
45 catciso.s . . . . . . . . . 10 𝑆 = (Baseβ€˜π‘Œ)
46 relfunc 17683 . . . . . . . . . . . 12 Rel (π‘Œ Func 𝑋)
4729simp2d 1144 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ(Hom β€˜πΆ)𝑋))
485, 2, 4, 25, 9, 8catchom 17924 . . . . . . . . . . . . . 14 (πœ‘ β†’ (π‘Œ(Hom β€˜πΆ)𝑋) = (π‘Œ Func 𝑋))
4948adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (π‘Œ(Hom β€˜πΆ)𝑋) = (π‘Œ Func 𝑋))
5047, 49eleqtrd 2841 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ Func 𝑋))
51 1st2ndbr 7964 . . . . . . . . . . . 12 ((Rel (π‘Œ Func 𝑋) ∧ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ Func 𝑋)) β†’ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))(π‘Œ Func 𝑋)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
5246, 50, 51sylancr 588 . . . . . . . . . . 11 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))(π‘Œ Func 𝑋)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
5352adantr 482 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))(π‘Œ Func 𝑋)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
5438, 45, 41funcf1 17687 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (1st β€˜πΉ):π‘…βŸΆπ‘†)
5554, 42ffvelcdmd 7031 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜πΉ)β€˜π‘₯) ∈ 𝑆)
5654, 43ffvelcdmd 7031 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜πΉ)β€˜π‘¦) ∈ 𝑆)
5745, 40, 39, 53, 55, 56funcf2 17689 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦)):(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦))⟢(((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯))(Hom β€˜π‘‹)((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦))))
5829simp3d 1145 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑋)𝐹) = ((Idβ€˜πΆ)β€˜π‘‹))
594adantr 482 . . . . . . . . . . . . . . . . 17 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ π‘ˆ ∈ 𝑉)
605, 2, 59, 26, 15, 16, 15, 33, 50catcco 17926 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(βŸ¨π‘‹, π‘ŒβŸ©(compβ€˜πΆ)𝑋)𝐹) = (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))
61 eqid 2738 . . . . . . . . . . . . . . . . . 18 (idfuncβ€˜π‘‹) = (idfuncβ€˜π‘‹)
625, 2, 27, 61, 4, 8catcid 17928 . . . . . . . . . . . . . . . . 17 (πœ‘ β†’ ((Idβ€˜πΆ)β€˜π‘‹) = (idfuncβ€˜π‘‹))
6362adantr 482 . . . . . . . . . . . . . . . 16 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((Idβ€˜πΆ)β€˜π‘‹) = (idfuncβ€˜π‘‹))
6458, 60, 633eqtr3d 2786 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹) = (idfuncβ€˜π‘‹))
6564adantr 482 . . . . . . . . . . . . . 14 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹) = (idfuncβ€˜π‘‹))
6665fveq2d 6842 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹)) = (1st β€˜(idfuncβ€˜π‘‹)))
6766fveq1d 6840 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))β€˜π‘₯) = ((1st β€˜(idfuncβ€˜π‘‹))β€˜π‘₯))
6833adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝐹 ∈ (𝑋 Func π‘Œ))
6950adantr 482 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ Func 𝑋))
7038, 68, 69, 42cofu1 17705 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))β€˜π‘₯) = ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯)))
715, 2, 4catcbas 17922 . . . . . . . . . . . . . . . 16 (πœ‘ β†’ 𝐡 = (π‘ˆ ∩ Cat))
72 inss2 4188 . . . . . . . . . . . . . . . 16 (π‘ˆ ∩ Cat) βŠ† Cat
7371, 72eqsstrdi 3997 . . . . . . . . . . . . . . 15 (πœ‘ β†’ 𝐡 βŠ† Cat)
7473, 8sseldd 3944 . . . . . . . . . . . . . 14 (πœ‘ β†’ 𝑋 ∈ Cat)
7574ad2antrr 725 . . . . . . . . . . . . 13 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝑋 ∈ Cat)
7661, 38, 75, 42idfu1 17701 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(idfuncβ€˜π‘‹))β€˜π‘₯) = π‘₯)
7767, 70, 763eqtr3d 2786 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯)) = π‘₯)
7866fveq1d 6840 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))β€˜π‘¦) = ((1st β€˜(idfuncβ€˜π‘‹))β€˜π‘¦))
7938, 68, 69, 43cofu1 17705 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))β€˜π‘¦) = ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦)))
8061, 38, 75, 43idfu1 17701 . . . . . . . . . . . 12 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜(idfuncβ€˜π‘‹))β€˜π‘¦) = 𝑦)
8178, 79, 803eqtr3d 2786 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦)) = 𝑦)
8277, 81oveq12d 7368 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯))(Hom β€˜π‘‹)((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦))) = (π‘₯(Hom β€˜π‘‹)𝑦))
8382feq3d 6651 . . . . . . . . 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 231 . . . . . . . 8 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦)):(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦))⟢(π‘₯(Hom β€˜π‘‹)𝑦))
8565fveq2d 6842 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (2nd β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹)) = (2nd β€˜(idfuncβ€˜π‘‹)))
8685oveqd 7367 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(2nd β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))𝑦) = (π‘₯(2nd β€˜(idfuncβ€˜π‘‹))𝑦))
8738, 68, 69, 42, 43cofu2nd 17706 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(2nd β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹))𝑦) = ((((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦)) ∘ (π‘₯(2nd β€˜πΉ)𝑦)))
8861, 38, 75, 39, 42, 43idfu2nd 17698 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(2nd β€˜(idfuncβ€˜π‘‹))𝑦) = ( I β†Ύ (π‘₯(Hom β€˜π‘‹)𝑦)))
8986, 87, 883eqtr3d 2786 . . . . . . . 8 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦)) ∘ (π‘₯(2nd β€˜πΉ)𝑦)) = ( I β†Ύ (π‘₯(Hom β€˜π‘‹)𝑦)))
9023simprd 497 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(π‘Œ(Sectβ€˜πΆ)𝑋)𝐹)
912, 25, 26, 27, 21, 14, 16, 15issect 17571 . . . . . . . . . . . . . . 15 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)(π‘Œ(Sectβ€˜πΆ)𝑋)𝐹 ↔ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ(Hom β€˜πΆ)𝑋) ∧ 𝐹 ∈ (𝑋(Hom β€˜πΆ)π‘Œ) ∧ (𝐹(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = ((Idβ€˜πΆ)β€˜π‘Œ))))
9290, 91mpbid 231 . . . . . . . . . . . . . 14 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∈ (π‘Œ(Hom β€˜πΆ)𝑋) ∧ 𝐹 ∈ (𝑋(Hom β€˜πΆ)π‘Œ) ∧ (𝐹(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = ((Idβ€˜πΆ)β€˜π‘Œ)))
9392simp3d 1145 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = ((Idβ€˜πΆ)β€˜π‘Œ))
945, 2, 59, 26, 16, 15, 16, 50, 33catcco 17926 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹(βŸ¨π‘Œ, π‘‹βŸ©(compβ€˜πΆ)π‘Œ)((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = (𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))
95 eqid 2738 . . . . . . . . . . . . . . 15 (idfuncβ€˜π‘Œ) = (idfuncβ€˜π‘Œ)
965, 2, 27, 95, 4, 9catcid 17928 . . . . . . . . . . . . . 14 (πœ‘ β†’ ((Idβ€˜πΆ)β€˜π‘Œ) = (idfuncβ€˜π‘Œ))
9796adantr 482 . . . . . . . . . . . . 13 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((Idβ€˜πΆ)β€˜π‘Œ) = (idfuncβ€˜π‘Œ))
9893, 94, 973eqtr3d 2786 . . . . . . . . . . . 12 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = (idfuncβ€˜π‘Œ))
9998adantr 482 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) = (idfuncβ€˜π‘Œ))
10099fveq2d 6842 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (2nd β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))) = (2nd β€˜(idfuncβ€˜π‘Œ)))
101100oveqd 7367 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))((1st β€˜πΉ)β€˜π‘¦)) = (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜(idfuncβ€˜π‘Œ))((1st β€˜πΉ)β€˜π‘¦)))
10245, 69, 68, 55, 56cofu2nd 17706 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))((1st β€˜πΉ)β€˜π‘¦)) = ((((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯))(2nd β€˜πΉ)((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦))) ∘ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦))))
10377, 81oveq12d 7368 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯))(2nd β€˜πΉ)((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦))) = (π‘₯(2nd β€˜πΉ)𝑦))
104103coeq1d 5814 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘₯))(2nd β€˜πΉ)((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))β€˜((1st β€˜πΉ)β€˜π‘¦))) ∘ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦))) = ((π‘₯(2nd β€˜πΉ)𝑦) ∘ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦))))
105102, 104eqtrd 2778 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)))((1st β€˜πΉ)β€˜π‘¦)) = ((π‘₯(2nd β€˜πΉ)𝑦) ∘ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦))))
10673ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ 𝐡 βŠ† Cat)
1079ad2antrr 725 . . . . . . . . . . 11 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ π‘Œ ∈ 𝐡)
108106, 107sseldd 3944 . . . . . . . . . 10 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ π‘Œ ∈ Cat)
10995, 45, 108, 40, 55, 56idfu2nd 17698 . . . . . . . . 9 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜(idfuncβ€˜π‘Œ))((1st β€˜πΉ)β€˜π‘¦)) = ( I β†Ύ (((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦))))
110101, 105, 1093eqtr3d 2786 . . . . . . . 8 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ ((π‘₯(2nd β€˜πΉ)𝑦) ∘ (((1st β€˜πΉ)β€˜π‘₯)(2nd β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))((1st β€˜πΉ)β€˜π‘¦))) = ( I β†Ύ (((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦))))
11144, 84, 89, 110fcof1od 7235 . . . . . . 7 (((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) ∧ (π‘₯ ∈ 𝑅 ∧ 𝑦 ∈ 𝑅)) β†’ (π‘₯(2nd β€˜πΉ)𝑦):(π‘₯(Hom β€˜π‘‹)𝑦)–1-1-ontoβ†’(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦)))
112111ralrimivva 3196 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ βˆ€π‘₯ ∈ 𝑅 βˆ€π‘¦ ∈ 𝑅 (π‘₯(2nd β€˜πΉ)𝑦):(π‘₯(Hom β€˜π‘‹)𝑦)–1-1-ontoβ†’(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦)))
11338, 39, 40isffth2 17738 . . . . . 6 ((1st β€˜πΉ)((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ))(2nd β€˜πΉ) ↔ ((1st β€˜πΉ)(𝑋 Func π‘Œ)(2nd β€˜πΉ) ∧ βˆ€π‘₯ ∈ 𝑅 βˆ€π‘¦ ∈ 𝑅 (π‘₯(2nd β€˜πΉ)𝑦):(π‘₯(Hom β€˜π‘‹)𝑦)–1-1-ontoβ†’(((1st β€˜πΉ)β€˜π‘₯)(Hom β€˜π‘Œ)((1st β€˜πΉ)β€˜π‘¦))))
11437, 112, 113sylanbrc 584 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜πΉ)((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ))(2nd β€˜πΉ))
115 df-br 5105 . . . . 5 ((1st β€˜πΉ)((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ))(2nd β€˜πΉ) ↔ ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩ ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)))
116114, 115sylib 217 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩ ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)))
11735, 116eqeltrd 2839 . . 3 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)))
11838, 45, 37funcf1 17687 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜πΉ):π‘…βŸΆπ‘†)
11945, 38, 52funcf1 17687 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)):π‘†βŸΆπ‘…)
12064fveq2d 6842 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹)) = (1st β€˜(idfuncβ€˜π‘‹)))
12138, 33, 50cofu1st 17704 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ) ∘func 𝐹)) = ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) ∘ (1st β€˜πΉ)))
12274adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ 𝑋 ∈ Cat)
12361, 38, 122idfu1st 17700 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(idfuncβ€˜π‘‹)) = ( I β†Ύ 𝑅))
124120, 121, 1233eqtr3d 2786 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ)) ∘ (1st β€˜πΉ)) = ( I β†Ύ 𝑅))
12598fveq2d 6842 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))) = (1st β€˜(idfuncβ€˜π‘Œ)))
12645, 50, 33cofu1st 17704 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(𝐹 ∘func ((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))) = ((1st β€˜πΉ) ∘ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))))
12773, 9sseldd 3944 . . . . . . 7 (πœ‘ β†’ π‘Œ ∈ Cat)
128127adantr 482 . . . . . 6 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ π‘Œ ∈ Cat)
12995, 45, 128idfu1st 17700 . . . . 5 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜(idfuncβ€˜π‘Œ)) = ( I β†Ύ 𝑆))
130125, 126, 1293eqtr3d 2786 . . . 4 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ ((1st β€˜πΉ) ∘ (1st β€˜((𝑋(Invβ€˜πΆ)π‘Œ)β€˜πΉ))) = ( I β†Ύ 𝑆))
131118, 119, 124, 130fcof1od 7235 . . 3 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)
132117, 131jca 513 . 2 ((πœ‘ ∧ 𝐹 ∈ (π‘‹πΌπ‘Œ)) β†’ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆))
1337adantr 482 . . 3 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐢 ∈ Cat)
1348adantr 482 . . 3 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝑋 ∈ 𝐡)
1359adantr 482 . . 3 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ π‘Œ ∈ 𝐡)
136 inss1 4187 . . . . . . 7 ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) βŠ† (𝑋 Full π‘Œ)
137 fullfunc 17728 . . . . . . 7 (𝑋 Full π‘Œ) βŠ† (𝑋 Func π‘Œ)
138136, 137sstri 3952 . . . . . 6 ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) βŠ† (𝑋 Func π‘Œ)
139 simprl 770 . . . . . 6 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)))
140138, 139sselid 3941 . . . . 5 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐹 ∈ (𝑋 Func π‘Œ))
1411, 140, 34sylancr 588 . . . 4 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐹 = ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩)
1424adantr 482 . . . . 5 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ π‘ˆ ∈ 𝑉)
143 eqid 2738 . . . . 5 (π‘₯ ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ β—‘((β—‘(1st β€˜πΉ)β€˜π‘₯)(2nd β€˜πΉ)(β—‘(1st β€˜πΉ)β€˜π‘¦))) = (π‘₯ ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ β—‘((β—‘(1st β€˜πΉ)β€˜π‘₯)(2nd β€˜πΉ)(β—‘(1st β€˜πΉ)β€˜π‘¦)))
144141, 139eqeltrrd 2840 . . . . . 6 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩ ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)))
145144, 115sylibr 233 . . . . 5 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ (1st β€˜πΉ)((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ))(2nd β€˜πΉ))
146 simprr 772 . . . . 5 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)
1475, 2, 38, 45, 142, 134, 135, 3, 143, 145, 146catcisolem 17931 . . . 4 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ ⟨(1st β€˜πΉ), (2nd β€˜πΉ)⟩(𝑋(Invβ€˜πΆ)π‘Œ)βŸ¨β—‘(1st β€˜πΉ), (π‘₯ ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ β—‘((β—‘(1st β€˜πΉ)β€˜π‘₯)(2nd β€˜πΉ)(β—‘(1st β€˜πΉ)β€˜π‘¦)))⟩)
148141, 147eqbrtrd 5126 . . 3 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐹(𝑋(Invβ€˜πΆ)π‘Œ)βŸ¨β—‘(1st β€˜πΉ), (π‘₯ ∈ 𝑆, 𝑦 ∈ 𝑆 ↦ β—‘((β—‘(1st β€˜πΉ)β€˜π‘₯)(2nd β€˜πΉ)(β—‘(1st β€˜πΉ)β€˜π‘¦)))⟩)
1492, 3, 133, 134, 135, 10, 148inviso1 17584 . 2 ((πœ‘ ∧ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)) β†’ 𝐹 ∈ (π‘‹πΌπ‘Œ))
150132, 149impbida 800 1 (πœ‘ β†’ (𝐹 ∈ (π‘‹πΌπ‘Œ) ↔ (𝐹 ∈ ((𝑋 Full π‘Œ) ∩ (𝑋 Faith π‘Œ)) ∧ (1st β€˜πΉ):𝑅–1-1-onto→𝑆)))
Colors of variables: wff setvar class
Syntax hints:   β†’ wi 4   ↔ wb 205   ∧ wa 397   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  βˆ€wral 3063   ∩ cin 3908   βŠ† wss 3909  βŸ¨cop 4591   class class class wbr 5104   I cid 5528  β—‘ccnv 5630  dom cdm 5631   β†Ύ cres 5633   ∘ ccom 5635  Rel wrel 5636  Fun wfun 6486  βŸΆwf 6488  β€“1-1-ontoβ†’wf1o 6491  β€˜cfv 6492  (class class class)co 7350   ∈ cmpo 7352  1st c1st 7910  2nd c2nd 7911  Basecbs 17018  Hom chom 17079  compcco 17080  Catccat 17479  Idccid 17480  Sectcsect 17562  Invcinv 17563  Isociso 17564   Func cfunc 17675  idfunccidfu 17676   ∘func ccofu 17677   Full cful 17724   Faith cfth 17725  CatCatccatc 17919
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2709  ax-rep 5241  ax-sep 5255  ax-nul 5262  ax-pow 5319  ax-pr 5383  ax-un 7663  ax-cnex 11041  ax-resscn 11042  ax-1cn 11043  ax-icn 11044  ax-addcl 11045  ax-addrcl 11046  ax-mulcl 11047  ax-mulrcl 11048  ax-mulcom 11049  ax-addass 11050  ax-mulass 11051  ax-distr 11052  ax-i2m1 11053  ax-1ne0 11054  ax-1rid 11055  ax-rnegex 11056  ax-rrecex 11057  ax-cnre 11058  ax-pre-lttri 11059  ax-pre-lttrn 11060  ax-pre-ltadd 11061  ax-pre-mulgt0 11062
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3or 1089  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2540  df-eu 2569  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2888  df-ne 2943  df-nel 3049  df-ral 3064  df-rex 3073  df-rmo 3352  df-reu 3353  df-rab 3407  df-v 3446  df-sbc 3739  df-csb 3855  df-dif 3912  df-un 3914  df-in 3916  df-ss 3926  df-pss 3928  df-nul 4282  df-if 4486  df-pw 4561  df-sn 4586  df-pr 4588  df-tp 4590  df-op 4592  df-uni 4865  df-iun 4955  df-br 5105  df-opab 5167  df-mpt 5188  df-tr 5222  df-id 5529  df-eprel 5535  df-po 5543  df-so 5544  df-fr 5586  df-we 5588  df-xp 5637  df-rel 5638  df-cnv 5639  df-co 5640  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644  df-pred 6250  df-ord 6317  df-on 6318  df-lim 6319  df-suc 6320  df-iota 6444  df-fun 6494  df-fn 6495  df-f 6496  df-f1 6497  df-fo 6498  df-f1o 6499  df-fv 6500  df-riota 7306  df-ov 7353  df-oprab 7354  df-mpo 7355  df-om 7794  df-1st 7912  df-2nd 7913  df-frecs 8180  df-wrecs 8211  df-recs 8285  df-rdg 8324  df-1o 8380  df-er 8582  df-map 8701  df-ixp 8770  df-en 8818  df-dom 8819  df-sdom 8820  df-fin 8821  df-pnf 11125  df-mnf 11126  df-xr 11127  df-ltxr 11128  df-le 11129  df-sub 11321  df-neg 11322  df-nn 12088  df-2 12150  df-3 12151  df-4 12152  df-5 12153  df-6 12154  df-7 12155  df-8 12156  df-9 12157  df-n0 12348  df-z 12434  df-dec 12552  df-uz 12697  df-fz 13354  df-struct 16954  df-slot 16989  df-ndx 17001  df-base 17019  df-hom 17092  df-cco 17093  df-cat 17483  df-cid 17484  df-sect 17565  df-inv 17566  df-iso 17567  df-func 17679  df-idfu 17680  df-cofu 17681  df-full 17726  df-fth 17727  df-catc 17920
This theorem is referenced by:  yoniso  18109  thincciso  46824
  Copyright terms: Public domain W3C validator