Theorem func1st2nd 49635

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

Syntax hints:   → wi 4   ∈ wcel 2132   class class class wbr 5090  Rel wrel 5641  ‘cfv 6506  (class class class)co 7381  1^st c1st 7953  2^nd c2nd 7954   Func cfunc 17859

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1805  ax-4 1819  ax-5 1920  ax-6 1977  ax-7 2018  ax-8 2134  ax-9 2142  ax-10 2165  ax-11 2181  ax-12 2202  ax-ext 2724  ax-sep 5236  ax-nul 5246  ax-pr 5380  ax-un 7703

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 857  df-3an 1097  df-tru 1553  df-fal 1563  df-ex 1790  df-nf 1794  df-sb 2081  df-mo 2556  df-eu 2586  df-clab 2731  df-cleq 2744  df-clel 2827  df-nfc 2901  df-ne 2948  df-ral 3067  df-rex 3077  df-rab 3405  df-v 3446  df-sbc 3736  df-csb 3844  df-dif 3898  df-un 3900  df-in 3902  df-ss 3912  df-nul 4277  df-if 4471  df-sn 4573  df-pr 4575  df-op 4579  df-uni 4856  df-iun 4941  df-br 5091  df-opab 5153  df-mpt 5172  df-id 5531  df-xp 5642  df-rel 5643  df-cnv 5644  df-co 5645  df-dm 5646  df-rn 5647  df-res 5648  df-ima 5649  df-iota 6462  df-fun 6508  df-fv 6514  df-ov 7384  df-oprab 7385  df-mpo 7386  df-1st 7955  df-2nd 7956  df-func 17863

This theorem is referenced by:  func0g2  49649  idfu1stalem  49659  idfu2nda  49662  cofid1a  49671  cofid2a  49672  cofidvala  49675  cofidf2a  49676  cofidf1a  49677  oppfoppc2  49701  funcoppc4  49703  2oppffunc  49705  cofuoppf  49709  idfth  49717  idsubc  49719  uppropd  49740  uptrlem2  49770  uptra  49774  uptrar  49775  uobeqw  49778  uobeq  49779  uptr2a  49781  natoppfb  49790  diag1f1  49866  diag2f1  49868  fuco11b  49896  fucocolem1  49912  fucocolem2  49913  fucocolem3  49914  fucocolem4  49915  fucoco  49916  fucolid  49920  fucorid  49921  fucorid2  49922  postcofval  49923  postcofcl  49924  precofval  49926  precofval2  49928  precofcl  49929  prcoftposcurfucoa  49943  prcof1  49947  prcof2a  49948  prcof2  49949  prcof22a  49951  prcofdiag1  49952  prcofdiag  49953  fucoppclem  49966  fucoppcid  49967  fucoppcco  49968  oppfdiag1  49973  oppfdiag  49975  isinito2lem  50057  termcfuncval  50091  diag1f1olem  50092  diagffth  50097  funcsn  50100  cofuterm  50104  uobeqterm  50105  isinito4  50106  lanval  50178  ranval  50179  lanup  50200  ranup  50201  lmdpropd  50216  cmdpropd  50217  islmd  50224  iscmd  50225  lmddu  50226  termolmd  50229  lmdran  50230  cmdlan  50231