oppf1 - Mathbox for Zhi Wang

	Mathbox for Zhi Wang		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > oppf1		Structured version Visualization version GIF version

Theorem oppf1 49769

Description: Value of the object part of the opposite functor. (Contributed by Zhi Wang, 19-Nov-2025.)

**Hypothesis**
Ref	Expression
oppf1.f	⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))

**Assertion**
Ref	Expression
oppf1	⊢ (𝜑 → (1^st ‘( oppFunc ‘𝐹)) = (1^st ‘𝐹))

**Proof of Theorem oppf1**
Step	Hyp	Ref	Expression
1		oppf1.f	. 2 ⊢ (𝜑 → 𝐹 ∈ (𝐶 Func 𝐷))
2		oppfval2 49767	. 2 ⊢ (𝐹 ∈ (𝐶 Func 𝐷) → ( oppFunc ‘𝐹) = ⟨(1^st ‘𝐹), tpos (2^nd ‘𝐹)⟩)
3		fvex 6884	. . 3 ⊢ (1^st ‘𝐹) ∈ V
4		fvex 6884	. . . 4 ⊢ (2^nd ‘𝐹) ∈ V
5	4	tposex 8244	. . 3 ⊢ tpos (2^nd ‘𝐹) ∈ V
6	3, 5	op1std 7984	. 2 ⊢ (( oppFunc ‘𝐹) = ⟨(1^st ‘𝐹), tpos (2^nd ‘𝐹)⟩ → (1^st ‘( oppFunc ‘𝐹)) = (1^st ‘𝐹))
7	1, 2, 6	3syl 19	1 ⊢ (𝜑 → (1^st ‘( oppFunc ‘𝐹)) = (1^st ‘𝐹))

Colors of variables: wff setvar class

Syntax hints: → wi 4 = wceq 1563 ∈ wcel 2145 ⟨cop 4591 ‘cfv 6525 (class class class)co 7400 1^st c1st 7972 2^nd c2nd 7973 tpos ctpos 8209 Func cfunc 17899 oppFunc coppf 49752

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1818 ax-4 1832 ax-5 1933 ax-6 1990 ax-7 2031 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2215 ax-ext 2737 ax-rep 5231 ax-sep 5250 ax-nul 5260 ax-pow 5326 ax-pr 5394 ax-un 7722

This theorem depends on definitions: df-bi 210 df-an 401 df-or 861 df-3an 1103 df-tru 1566 df-fal 1576 df-ex 1803 df-nf 1807 df-sb 2094 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-ral 3080 df-rex 3090 df-rab 3418 df-v 3459 df-sbc 3748 df-csb 3856 df-dif 3910 df-un 3912 df-in 3914 df-ss 3924 df-nul 4289 df-if 4484 df-pw 4560 df-sn 4586 df-pr 4588 df-op 4592 df-uni 4868 df-iun 4953 df-br 5105 df-opab 5167 df-mpt 5186 df-id 5546 df-xp 5657 df-rel 5658 df-cnv 5659 df-co 5660 df-dm 5661 df-rn 5662 df-res 5663 df-ima 5664 df-iota 6481 df-fun 6527 df-fn 6528 df-f 6529 df-fv 6533 df-ov 7403 df-oprab 7404 df-mpo 7405 df-1st 7974 df-2nd 7975 df-tpos 8210 df-map 8814 df-ixp 8884 df-func 17903 df-oppf 49753

This theorem is referenced by: oppfdiag1 50044 oppfdiag 50046 lmddu 50297 lmdran 50301

W3C validator