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

Theorem issubc 13712
 Description: Elementhood in the set of subcategories. (Contributed by Mario Carneiro, 4-Jan-2017.)
Hypotheses
Ref Expression
issubc.h f
issubc.i
issubc.o comp
issubc.c
issubc.s
Assertion
Ref Expression
issubc Subcat cat
Distinct variable groups:   ,,,,,   ,,,,,   ,,,,,
Allowed substitution hints:   (,,,,)   (,,,,)   (,,,,)   (,,,,)

Proof of Theorem issubc
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 issubc.c . 2
2 issubc.s . 2
3 simpl 443 . . . . 5
4 sscpwex 13692 . . . . . . . 8 cat f
5 simpl 443 . . . . . . . . 9 cat f comp cat f
65ss2abi 3245 . . . . . . . 8 cat f comp cat f
74, 6ssexi 4159 . . . . . . 7 cat f comp
87ax-gen 1533 . . . . . 6 cat f comp
9 csbexg 3091 . . . . . 6 cat f comp cat f comp
103, 8, 9sylancl 643 . . . . 5 cat f comp
11 df-subc 13689 . . . . . 6 Subcat cat f comp
1211fvmpts 5603 . . . . 5 cat f comp Subcat cat f comp
133, 10, 12syl2anc 642 . . . 4 Subcat cat f comp
1413eleq2d 2350 . . 3 Subcat cat f comp
15 sbcel2g 3102 . . . 4 cat f comp cat f comp
163, 15syl 15 . . 3 cat f comp cat f comp
17 elex 2796 . . . . . 6 cat f comp
1817a1i 10 . . . . 5 cat f comp
19 sscrel 13690 . . . . . . . 8 cat
2019brrelexi 4729 . . . . . . 7 cat
2120adantr 451 . . . . . 6 cat
2221a1i 10 . . . . 5 cat
23 df-sbc 2992 . . . . . . 7 cat f comp cat f comp
24 simpr 447 . . . . . . . 8
25 simpr 447 . . . . . . . . . . 11
26 simpr 447 . . . . . . . . . . . . . 14
2726fveq2d 5529 . . . . . . . . . . . . 13 f f
28 issubc.h . . . . . . . . . . . . 13 f
2927, 28syl6eqr 2333 . . . . . . . . . . . 12 f
3029adantr 451 . . . . . . . . . . 11 f
3125, 30breq12d 4036 . . . . . . . . . 10 cat f cat
32 vex 2791 . . . . . . . . . . . . . 14
3332dmex 4941 . . . . . . . . . . . . 13
3433dmex 4941 . . . . . . . . . . . 12
3534a1i 10 . . . . . . . . . . 11
3625dmeqd 4881 . . . . . . . . . . . . 13
3736dmeqd 4881 . . . . . . . . . . . 12
38 simpr 447 . . . . . . . . . . . . 13
3938ad2antrr 706 . . . . . . . . . . . 12
4037, 39eqtr4d 2318 . . . . . . . . . . 11
41 simpr 447 . . . . . . . . . . . 12
42 simpllr 735 . . . . . . . . . . . . . . . . 17
4342fveq2d 5529 . . . . . . . . . . . . . . . 16
44 issubc.i . . . . . . . . . . . . . . . 16
4543, 44syl6eqr 2333 . . . . . . . . . . . . . . 15
4645fveq1d 5527 . . . . . . . . . . . . . 14
47 simplr 731 . . . . . . . . . . . . . . 15
4847oveqd 5875 . . . . . . . . . . . . . 14
4946, 48eleq12d 2351 . . . . . . . . . . . . 13
5047oveqd 5875 . . . . . . . . . . . . . . . 16
5147oveqd 5875 . . . . . . . . . . . . . . . . 17
5242fveq2d 5529 . . . . . . . . . . . . . . . . . . . . 21 comp comp
53 issubc.o . . . . . . . . . . . . . . . . . . . . 21 comp
5452, 53syl6eqr 2333 . . . . . . . . . . . . . . . . . . . 20 comp
5554oveqd 5875 . . . . . . . . . . . . . . . . . . 19 comp
5655oveqd 5875 . . . . . . . . . . . . . . . . . 18 comp
5747oveqd 5875 . . . . . . . . . . . . . . . . . 18
5856, 57eleq12d 2351 . . . . . . . . . . . . . . . . 17 comp
5951, 58raleqbidv 2748 . . . . . . . . . . . . . . . 16 comp
6050, 59raleqbidv 2748 . . . . . . . . . . . . . . 15 comp
6141, 60raleqbidv 2748 . . . . . . . . . . . . . 14 comp
6241, 61raleqbidv 2748 . . . . . . . . . . . . 13 comp
6349, 62anbi12d 691 . . . . . . . . . . . 12 comp
6441, 63raleqbidv 2748 . . . . . . . . . . 11 comp
6535, 40, 64sbcied2 3028 . . . . . . . . . 10 comp
6631, 65anbi12d 691 . . . . . . . . 9 cat f comp cat
6766adantlr 695 . . . . . . . 8 cat f comp cat
6824, 67sbcied 3027 . . . . . . 7 cat f comp cat
6923, 68syl5bbr 250 . . . . . 6 cat f comp cat
7069ex 423 . . . . 5 cat f comp cat
7118, 22, 70pm5.21ndd 343 . . . 4 cat f comp cat
723, 71sbcied 3027 . . 3 cat f comp cat
7314, 16, 723bitr2d 272 . 2 Subcat cat
741, 2, 73syl2anc 642 1 Subcat cat
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358  wal 1527   wceq 1623   wcel 1684  cab 2269  wral 2543  cvv 2788  wsbc 2991  csb 3081  cop 3643   class class class wbr 4023   cdm 4689  cfv 5255  (class class class)co 5858  compcco 13220  ccat 13566  ccid 13567   f chomf 13568   cat cssc 13684  Subcatcsubc 13686 This theorem is referenced by:  issubc2  13713  subcssc  13714 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-pm 6775  df-ixp 6818  df-ssc 13687  df-subc 13689
 Copyright terms: Public domain W3C validator