Theorem func1st2nd 50395

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2147   class class class wbr 5106  Rel wrel 5660  ‘cfv 6558  (class class class)co 7443  1^st c1st 8023  2^nd c2nd 8024   Func cfunc 18058

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-10 2180  ax-11 2197  ax-12 2216  ax-ext 2735  ax-sep 5252  ax-nul 5263  ax-pr 5395  ax-un 7775

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-nf 1817  df-sb 2102  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2839  df-nfc 2913  df-ne 2960  df-ral 3081  df-rex 3091  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-uni 4871  df-br 5107  df-opab 5171  df-mpt 5190  df-id 5550  df-xp 5661  df-rel 5662  df-cnv 5663  df-co 5664  df-dm 5665  df-rn 5666  df-iota 6512  df-fun 6560  df-fv 6566  df-ov 7446  df-oprab 7447  df-mpo 7448  df-1st 8025  df-2nd 8026  df-func 18062

This theorem is used by:  func0g2  50410  cofu1stfix  50417  idfu1stalem  50421  idfu2nda  50424  cofid1a  50433  cofid2a  50434  cofidvala  50437  cofidf2a  50438  cofidf1a  50439  oppfoppc2  50463  funcoppc4  50465  2oppffunc  50467  cofuoppf  50471  idfth  50479  idsubc  50481  uppropd  50502  uptrlem2  50532  uptra  50536  uptrar  50537  uobeqw  50540  uobeq  50541  uptr2a  50543  natideq  50550  natoppfb  50558  diag1f1  50634  diag2f1  50636  fuco11b  50664  fucocolem1  50680  fucocolem2  50681  fucocolem3  50682  fucocolem4  50683  fucoco  50684  fucolid  50688  fucorid  50689  fucorid2  50690  fucoaltfunc  50696  postcofval  50701  postcofcl  50702  precofval  50707  precofval2  50709  precofcl  50710  prcoftposcurfucoa  50724  prcof1  50728  prcof2a  50729  prcof2  50730  prcof22a  50732  prcofdiag1  50733  prcofdiag  50734  fucoppclem  50747  fucoppcid  50748  fucoppcco  50749  oppfdiag1  50754  oppfdiag  50756  isinito2lem  50838  termcfuncval  50872  diag1f1olem  50873  termccofix  50876  diagffth  50881  funcsn  50884  cofuterm  50888  uobeqterm  50889  isinito4  50890  lanval  51007  ranval  51008  lanup  51029  ranup  51030  lmdpropd  51045  cmdpropd  51046  islmd  51053  iscmd  51054  lmddu  51055  termolmd  51058  lmdran  51059  cmdlan  51060