Theorem func1st2nd 49882

Description: Rewrite the functor predicate with separated parts. (Contributed by Zhi Wang, 19-Oct-2025.)

Hypothesis

Ref	Expression
func1st2nd.1	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))

Assertion

Ref	Expression
func1st2nd	⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

Proof of Theorem func1st2nd

Step	Hyp	Ref	Expression
1		relfunc 17925	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 8037	. 2 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
4	1, 2, 3	sylancr 598	1 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2142   class class class wbr 5108  Rel wrel 5665  ‘cfv 6536  (class class class)co 7412  1^st c1st 7982  2^nd c2nd 7983   Func cfunc 17917

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-10 2175  ax-11 2191  ax-12 2212  ax-ext 2734  ax-sep 5256  ax-nul 5268  ax-pr 5403  ax-un 7734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-nf 1813  df-sb 2096  df-mo 2566  df-eu 2596  df-clab 2741  df-cleq 2754  df-clel 2837  df-nfc 2911  df-ne 2958  df-ral 3079  df-rex 3089  df-rab 3416  df-v 3456  df-sbc 3744  df-csb 3853  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-uni 4872  df-iun 4957  df-br 5109  df-opab 5173  df-mpt 5192  df-id 5555  df-xp 5666  df-rel 5667  df-cnv 5668  df-co 5669  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673  df-iota 6492  df-fun 6538  df-fv 6544  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7984  df-2nd 7985  df-func 17921

This theorem is used by:  func0g2  49896  idfu1stalem  49906  idfu2nda  49909  cofid1a  49918  cofid2a  49919  cofidvala  49922  cofidf2a  49923  cofidf1a  49924  oppfoppc2  49948  funcoppc4  49950  2oppffunc  49952  cofuoppf  49956  idfth  49964  idsubc  49966  uppropd  49987  uptrlem2  50017  uptra  50021  uptrar  50022  uobeqw  50025  uobeq  50026  uptr2a  50028  natoppfb  50037  diag1f1  50113  diag2f1  50115  fuco11b  50143  fucocolem1  50159  fucocolem2  50160  fucocolem3  50161  fucocolem4  50162  fucoco  50163  fucolid  50167  fucorid  50168  fucorid2  50169  postcofval  50170  postcofcl  50171  precofval  50173  precofval2  50175  precofcl  50176  prcoftposcurfucoa  50190  prcof1  50194  prcof2a  50195  prcof2  50196  prcof22a  50198  prcofdiag1  50199  prcofdiag  50200  fucoppclem  50213  fucoppcid  50214  fucoppcco  50215  oppfdiag1  50220  oppfdiag  50222  isinito2lem  50304  termcfuncval  50338  diag1f1olem  50339  diagffth  50344  funcsn  50347  cofuterm  50351  uobeqterm  50352  isinito4  50353  lanval  50425  ranval  50426  lanup  50447  ranup  50448  lmdpropd  50463  cmdpropd  50464  islmd  50471  iscmd  50472  lmddu  50473  termolmd  50476  lmdran  50477  cmdlan  50478