Theorem func1st2nd 49688

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

Syntax hints:   → wi 4   ∈ wcel 2143   class class class wbr 5101  Rel wrel 5653  ‘cfv 6521  (class class class)co 7396  1^st c1st 7968  2^nd c2nd 7969   Func cfunc 17897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1816  ax-4 1830  ax-5 1931  ax-6 1988  ax-7 2029  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735  ax-sep 5247  ax-nul 5257  ax-pr 5391  ax-un 7718

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1101  df-tru 1564  df-fal 1574  df-ex 1801  df-nf 1805  df-sb 2092  df-mo 2567  df-eu 2597  df-clab 2742  df-cleq 2755  df-clel 2838  df-nfc 2912  df-ne 2959  df-ral 3078  df-rex 3088  df-rab 3416  df-v 3457  df-sbc 3746  df-csb 3854  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  df-uni 4867  df-iun 4952  df-br 5102  df-opab 5164  df-mpt 5183  df-id 5543  df-xp 5654  df-rel 5655  df-cnv 5656  df-co 5657  df-dm 5658  df-rn 5659  df-res 5660  df-ima 5661  df-iota 6477  df-fun 6523  df-fv 6529  df-ov 7399  df-oprab 7400  df-mpo 7401  df-1st 7970  df-2nd 7971  df-func 17901

This theorem is referenced by:  func0g2  49702  idfu1stalem  49712  idfu2nda  49715  cofid1a  49724  cofid2a  49725  cofidvala  49728  cofidf2a  49729  cofidf1a  49730  oppfoppc2  49754  funcoppc4  49756  2oppffunc  49758  cofuoppf  49762  idfth  49770  idsubc  49772  uppropd  49793  uptrlem2  49823  uptra  49827  uptrar  49828  uobeqw  49831  uobeq  49832  uptr2a  49834  natoppfb  49843  diag1f1  49919  diag2f1  49921  fuco11b  49949  fucocolem1  49965  fucocolem2  49966  fucocolem3  49967  fucocolem4  49968  fucoco  49969  fucolid  49973  fucorid  49974  fucorid2  49975  postcofval  49976  postcofcl  49977  precofval  49979  precofval2  49981  precofcl  49982  prcoftposcurfucoa  49996  prcof1  50000  prcof2a  50001  prcof2  50002  prcof22a  50004  prcofdiag1  50005  prcofdiag  50006  fucoppclem  50019  fucoppcid  50020  fucoppcco  50021  oppfdiag1  50026  oppfdiag  50028  isinito2lem  50110  termcfuncval  50144  diag1f1olem  50145  diagffth  50150  funcsn  50153  cofuterm  50157  uobeqterm  50158  isinito4  50159  lanval  50231  ranval  50232  lanup  50253  ranup  50254  lmdpropd  50269  cmdpropd  50270  islmd  50277  iscmd  50278  lmddu  50279  termolmd  50282  lmdran  50283  cmdlan  50284