Theorem func1st2nd 50106

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 17998	. 2 ⊢ Rel (𝐶 Func 𝐷)
2		func1st2nd.1	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
3		1st2ndbr 8036	. 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 2145   class class class wbr 5102  Rel wrel 5652  ‘cfv 6527  (class class class)co 7408  1^st c1st 7982  2^nd c2nd 7983   Func cfunc 17990

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-10 2178  ax-11 2194  ax-12 2213  ax-ext 2732  ax-sep 5248  ax-nul 5259  ax-pr 5390  ax-un 7734

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 2100  df-mo 2564  df-eu 2594  df-clab 2739  df-cleq 2752  df-clel 2835  df-nfc 2909  df-ne 2956  df-ral 3077  df-rex 3087  df-rab 3413  df-v 3452  df-sbc 3739  df-csb 3847  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5103  df-opab 5167  df-mpt 5186  df-id 5542  df-xp 5653  df-rel 5654  df-cnv 5655  df-co 5656  df-dm 5657  df-rn 5658  df-res 5659  df-ima 5660  df-iota 6483  df-fun 6529  df-fv 6535  df-ov 7411  df-oprab 7412  df-mpo 7413  df-1st 7984  df-2nd 7985  df-func 17994

This theorem is used by:  func0g2  50120  idfu1stalem  50130  idfu2nda  50133  cofid1a  50142  cofid2a  50143  cofidvala  50146  cofidf2a  50147  cofidf1a  50148  oppfoppc2  50172  funcoppc4  50174  2oppffunc  50176  cofuoppf  50180  idfth  50188  idsubc  50190  uppropd  50211  uptrlem2  50241  uptra  50245  uptrar  50246  uobeqw  50249  uobeq  50250  uptr2a  50252  natoppfb  50261  diag1f1  50337  diag2f1  50339  fuco11b  50367  fucocolem1  50383  fucocolem2  50384  fucocolem3  50385  fucocolem4  50386  fucoco  50387  fucolid  50391  fucorid  50392  fucorid2  50393  postcofval  50394  postcofcl  50395  precofval  50397  precofval2  50399  precofcl  50400  prcoftposcurfucoa  50414  prcof1  50418  prcof2a  50419  prcof2  50420  prcof22a  50422  prcofdiag1  50423  prcofdiag  50424  fucoppclem  50437  fucoppcid  50438  fucoppcco  50439  oppfdiag1  50444  oppfdiag  50446  isinito2lem  50528  termcfuncval  50562  diag1f1olem  50563  diagffth  50568  funcsn  50571  cofuterm  50575  uobeqterm  50576  isinito4  50577  lanval  50649  ranval  50650  lanup  50671  ranup  50672  lmdpropd  50687  cmdpropd  50688  islmd  50695  iscmd  50696  lmddu  50697  termolmd  50700  lmdran  50701  cmdlan  50702