Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  isfth Unicode version

Theorem isfth 13804
 Description: Value of the set of faithful functors between two categories. (Contributed by Mario Carneiro, 27-Jan-2017.)
Hypothesis
Ref Expression
isfth.b
Assertion
Ref Expression
isfth Faith
Distinct variable groups:   ,,   ,,   ,,   ,,   ,,

Proof of Theorem isfth
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 fthfunc 13797 . . 3 Faith
21ssbri 4081 . 2 Faith
3 df-br 4040 . . . . . . . 8
4 funcrcl 13753 . . . . . . . 8
53, 4sylbi 187 . . . . . . 7
6 oveq12 5883 . . . . . . . . . . 11
76breqd 4050 . . . . . . . . . 10
8 simpl 443 . . . . . . . . . . . . 13
98fveq2d 5545 . . . . . . . . . . . 12
10 isfth.b . . . . . . . . . . . 12
119, 10syl6eqr 2346 . . . . . . . . . . 11
1211raleqdv 2755 . . . . . . . . . . 11
1311, 12raleqbidv 2761 . . . . . . . . . 10
147, 13anbi12d 691 . . . . . . . . 9
1514opabbidv 4098 . . . . . . . 8
16 df-fth 13795 . . . . . . . 8 Faith
17 ovex 5899 . . . . . . . . 9
18 simpl 443 . . . . . . . . . . 11
1918ssopab2i 4308 . . . . . . . . . 10
20 opabss 4096 . . . . . . . . . 10
2119, 20sstri 3201 . . . . . . . . 9
2217, 21ssexi 4175 . . . . . . . 8
2315, 16, 22ovmpt2a 5994 . . . . . . 7 Faith
245, 23syl 15 . . . . . 6 Faith
2524breqd 4050 . . . . 5 Faith
26 relfunc 13752 . . . . . . 7
27 brrelex12 4742 . . . . . . 7
2826, 27mpan 651 . . . . . 6
29 breq12 4044 . . . . . . . 8
30 simpr 447 . . . . . . . . . . . 12
3130oveqd 5891 . . . . . . . . . . 11
3231cnveqd 4873 . . . . . . . . . 10
3332funeqd 5292 . . . . . . . . 9
34332ralbidv 2598 . . . . . . . 8
3529, 34anbi12d 691 . . . . . . 7
36 eqid 2296 . . . . . . 7
3735, 36brabga 4295 . . . . . 6
3828, 37syl 15 . . . . 5
3925, 38bitrd 244 . . . 4 Faith
4039baibd 875 . . 3 Faith
4140anidms 626 . 2 Faith