Theorem func1st2nd 49182

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 17775	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 7980	. 2 ⊢ ((Rel (𝐶 Func 𝐷) ∧ 𝐹 ∈ (𝐶 Func 𝐷)) → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))
4	1, 2, 3	sylancr 587	1 ⊢ (𝜑 → (1st ‘𝐹)(𝐶 Func 𝐷)(2nd ‘𝐹))

Syntax hints:   → wi 4   ∈ wcel 2111   class class class wbr 5093  Rel wrel 5624  ‘cfv 6487  (class class class)co 7352  1^st c1st 7925  2^nd c2nd 7926   Func cfunc 17767

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-10 2144  ax-11 2160  ax-12 2180  ax-ext 2703  ax-sep 5236  ax-nul 5246  ax-pr 5372  ax-un 7674

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-nf 1785  df-sb 2068  df-mo 2535  df-eu 2564  df-clab 2710  df-cleq 2723  df-clel 2806  df-nfc 2881  df-ne 2929  df-ral 3048  df-rex 3057  df-rab 3396  df-v 3438  df-sbc 3737  df-csb 3846  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-uni 4859  df-iun 4943  df-br 5094  df-opab 5156  df-mpt 5175  df-id 5514  df-xp 5625  df-rel 5626  df-cnv 5627  df-co 5628  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632  df-iota 6443  df-fun 6489  df-fv 6495  df-ov 7355  df-oprab 7356  df-mpo 7357  df-1st 7927  df-2nd 7928  df-func 17771

This theorem is referenced by:  func0g2  49196  idfu1stalem  49206  idfu2nda  49209  cofid1a  49218  cofid2a  49219  cofidvala  49222  cofidf2a  49223  cofidf1a  49224  oppfoppc2  49248  funcoppc4  49250  2oppffunc  49252  cofuoppf  49256  idfth  49264  idsubc  49266  uppropd  49287  uptrlem2  49317  uptra  49321  uptrar  49322  uobeqw  49325  uobeq  49326  uptr2a  49328  natoppfb  49337  diag1f1  49413  diag2f1  49415  fuco11b  49443  fucocolem1  49459  fucocolem2  49460  fucocolem3  49461  fucocolem4  49462  fucoco  49463  fucolid  49467  fucorid  49468  fucorid2  49469  postcofval  49470  postcofcl  49471  precofval  49473  precofval2  49475  precofcl  49476  prcoftposcurfucoa  49490  prcof1  49494  prcof2a  49495  prcof2  49496  prcof22a  49498  prcofdiag1  49499  prcofdiag  49500  fucoppclem  49513  fucoppcid  49514  fucoppcco  49515  oppfdiag1  49520  oppfdiag  49522  isinito2lem  49604  termcfuncval  49638  diag1f1olem  49639  diagffth  49644  funcsn  49647  cofuterm  49651  uobeqterm  49652  isinito4  49653  lanval  49725  ranval  49726  lanup  49747  ranup  49748  lmdpropd  49763  cmdpropd  49764  islmd  49771  iscmd  49772  lmddu  49773  termolmd  49776  lmdran  49777  cmdlan  49778