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

Theorem isfth 14103
 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 14096 . . 3 Faith
21ssbri 4246 . 2 Faith
3 df-br 4205 . . . . . . 7
4 funcrcl 14052 . . . . . . 7
53, 4sylbi 188 . . . . . 6
6 oveq12 6082 . . . . . . . . . 10
76breqd 4215 . . . . . . . . 9
8 simpl 444 . . . . . . . . . . . 12
98fveq2d 5724 . . . . . . . . . . 11
10 isfth.b . . . . . . . . . . 11
119, 10syl6eqr 2485 . . . . . . . . . 10
1211raleqdv 2902 . . . . . . . . . 10
1311, 12raleqbidv 2908 . . . . . . . . 9
147, 13anbi12d 692 . . . . . . . 8
1514opabbidv 4263 . . . . . . 7
16 df-fth 14094 . . . . . . 7 Faith
17 ovex 6098 . . . . . . . 8
18 simpl 444 . . . . . . . . . 10
1918ssopab2i 4474 . . . . . . . . 9
20 opabss 4261 . . . . . . . . 9
2119, 20sstri 3349 . . . . . . . 8
2217, 21ssexi 4340 . . . . . . 7
2315, 16, 22ovmpt2a 6196 . . . . . 6 Faith
245, 23syl 16 . . . . 5 Faith
2524breqd 4215 . . . 4 Faith
26 relfunc 14051 . . . . . 6
27 brrelex12 4907 . . . . . 6
2826, 27mpan 652 . . . . 5
29 breq12 4209 . . . . . . 7
30 simpr 448 . . . . . . . . . . 11
3130oveqd 6090 . . . . . . . . . 10
3231cnveqd 5040 . . . . . . . . 9
3332funeqd 5467 . . . . . . . 8
34332ralbidv 2739 . . . . . . 7
3529, 34anbi12d 692 . . . . . 6
36 eqid 2435 . . . . . 6
3735, 36brabga 4461 . . . . 5
3828, 37syl 16 . . . 4
3925, 38bitrd 245 . . 3 Faith
4039bianabs 851 . 2 Faith