phoeqi - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > phoeqi		Structured version Visualization version GIF version

Theorem phoeqi 27697

Description: A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.)

**Hypotheses**
Ref	Expression
ip2eqi.1	⊢ 𝑋 = (BaseSet‘𝑈)
ip2eqi.7	⊢ 𝑃 = (·_𝑖OLD‘𝑈)
ip2eqi.u	⊢ 𝑈 ∈ CPreHil_OLD

**Assertion**
Ref	Expression
phoeqi	⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))

Distinct variable groups: 𝑥,𝑃 𝑥,𝑦,𝑆 𝑥,𝑇,𝑦 𝑥,𝑈 𝑥,𝑋,𝑦 𝑥,𝑌,𝑦 Allowed substitution hints: 𝑃(𝑦) 𝑈(𝑦)

**Proof of Theorem phoeqi**
Step	Hyp	Ref	Expression
1		ralcom 3096	. 2 ⊢ (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ ∀𝑦 ∈ 𝑌 ∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)))
2		ffvelrn 6355	. . . . . 6 ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑆‘𝑦) ∈ 𝑋)
3		ffvelrn 6355	. . . . . 6 ⊢ ((𝑇:𝑌⟶𝑋 ∧ 𝑦 ∈ 𝑌) → (𝑇‘𝑦) ∈ 𝑋)
4		ip2eqi.1	. . . . . . 7 ⊢ 𝑋 = (BaseSet‘𝑈)
5		ip2eqi.7	. . . . . . 7 ⊢ 𝑃 = (·_𝑖OLD‘𝑈)
6		ip2eqi.u	. . . . . . 7 ⊢ 𝑈 ∈ CPreHil_OLD
7	4, 5, 6	ip2eqi 27696	. . . . . 6 ⊢ (((𝑆‘𝑦) ∈ 𝑋 ∧ (𝑇‘𝑦) ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ (𝑆‘𝑦) = (𝑇‘𝑦)))
8	2, 3, 7	syl2an 494	. . . . 5 ⊢ (((𝑆:𝑌⟶𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑇:𝑌⟶𝑋 ∧ 𝑦 ∈ 𝑌)) → (∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ (𝑆‘𝑦) = (𝑇‘𝑦)))
9	8	anandirs 874	. . . 4 ⊢ (((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) ∧ 𝑦 ∈ 𝑌) → (∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ (𝑆‘𝑦) = (𝑇‘𝑦)))
10	9	ralbidva 2984	. . 3 ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑦 ∈ 𝑌 ∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ ∀𝑦 ∈ 𝑌 (𝑆‘𝑦) = (𝑇‘𝑦)))
11		ffn 6043	. . . 4 ⊢ (𝑆:𝑌⟶𝑋 → 𝑆 Fn 𝑌)
12		ffn 6043	. . . 4 ⊢ (𝑇:𝑌⟶𝑋 → 𝑇 Fn 𝑌)
13		eqfnfv 6309	. . . 4 ⊢ ((𝑆 Fn 𝑌 ∧ 𝑇 Fn 𝑌) → (𝑆 = 𝑇 ↔ ∀𝑦 ∈ 𝑌 (𝑆‘𝑦) = (𝑇‘𝑦)))
14	11, 12, 13	syl2an 494	. . 3 ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (𝑆 = 𝑇 ↔ ∀𝑦 ∈ 𝑌 (𝑆‘𝑦) = (𝑇‘𝑦)))
15	10, 14	bitr4d 271	. 2 ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑦 ∈ 𝑌 ∀𝑥 ∈ 𝑋 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))
16	1, 15	syl5bb 272	1 ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ↔ wb 196 ∧ wa 384 = wceq 1482 ∈ wcel 1989 ∀wral 2911 Fn wfn 5881 ⟶wf 5882 ‘cfv 5886 (class class class)co 6647 BaseSetcba 27425 ·_𝑖OLDcdip 27539 CPreHil_OLDccphlo 27651

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1721 ax-4 1736 ax-5 1838 ax-6 1887 ax-7 1934 ax-8 1991 ax-9 1998 ax-10 2018 ax-11 2033 ax-12 2046 ax-13 2245 ax-ext 2601 ax-rep 4769 ax-sep 4779 ax-nul 4787 ax-pow 4841 ax-pr 4904 ax-un 6946 ax-inf2 8535 ax-cnex 9989 ax-resscn 9990 ax-1cn 9991 ax-icn 9992 ax-addcl 9993 ax-addrcl 9994 ax-mulcl 9995 ax-mulrcl 9996 ax-mulcom 9997 ax-addass 9998 ax-mulass 9999 ax-distr 10000 ax-i2m1 10001 ax-1ne0 10002 ax-1rid 10003 ax-rnegex 10004 ax-rrecex 10005 ax-cnre 10006 ax-pre-lttri 10007 ax-pre-lttrn 10008 ax-pre-ltadd 10009 ax-pre-mulgt0 10010 ax-pre-sup 10011 ax-addf 10012 ax-mulf 10013

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1485 df-fal 1488 df-ex 1704 df-nf 1709 df-sb 1880 df-eu 2473 df-mo 2474 df-clab 2608 df-cleq 2614 df-clel 2617 df-nfc 2752 df-ne 2794 df-nel 2897 df-ral 2916 df-rex 2917 df-reu 2918 df-rmo 2919 df-rab 2920 df-v 3200 df-sbc 3434 df-csb 3532 df-dif 3575 df-un 3577 df-in 3579 df-ss 3586 df-pss 3588 df-nul 3914 df-if 4085 df-pw 4158 df-sn 4176 df-pr 4178 df-tp 4180 df-op 4182 df-uni 4435 df-int 4474 df-iun 4520 df-iin 4521 df-br 4652 df-opab 4711 df-mpt 4728 df-tr 4751 df-id 5022 df-eprel 5027 df-po 5033 df-so 5034 df-fr 5071 df-se 5072 df-we 5073 df-xp 5118 df-rel 5119 df-cnv 5120 df-co 5121 df-dm 5122 df-rn 5123 df-res 5124 df-ima 5125 df-pred 5678 df-ord 5724 df-on 5725 df-lim 5726 df-suc 5727 df-iota 5849 df-fun 5888 df-fn 5889 df-f 5890 df-f1 5891 df-fo 5892 df-f1o 5893 df-fv 5894 df-isom 5895 df-riota 6608 df-ov 6650 df-oprab 6651 df-mpt2 6652 df-of 6894 df-om 7063 df-1st 7165 df-2nd 7166 df-supp 7293 df-wrecs 7404 df-recs 7465 df-rdg 7503 df-1o 7557 df-2o 7558 df-oadd 7561 df-er 7739 df-map 7856 df-ixp 7906 df-en 7953 df-dom 7954 df-sdom 7955 df-fin 7956 df-fsupp 8273 df-fi 8314 df-sup 8345 df-inf 8346 df-oi 8412 df-card 8762 df-cda 8987 df-pnf 10073 df-mnf 10074 df-xr 10075 df-ltxr 10076 df-le 10077 df-sub 10265 df-neg 10266 df-div 10682 df-nn 11018 df-2 11076 df-3 11077 df-4 11078 df-5 11079 df-6 11080 df-7 11081 df-8 11082 df-9 11083 df-n0 11290 df-z 11375 df-dec 11491 df-uz 11685 df-q 11786 df-rp 11830 df-xneg 11943 df-xadd 11944 df-xmul 11945 df-ioo 12176 df-icc 12179 df-fz 12324 df-fzo 12462 df-seq 12797 df-exp 12856 df-hash 13113 df-cj 13833 df-re 13834 df-im 13835 df-sqrt 13969 df-abs 13970 df-clim 14213 df-sum 14411 df-struct 15853 df-ndx 15854 df-slot 15855 df-base 15857 df-sets 15858 df-ress 15859 df-plusg 15948 df-mulr 15949 df-starv 15950 df-sca 15951 df-vsca 15952 df-ip 15953 df-tset 15954 df-ple 15955 df-ds 15958 df-unif 15959 df-hom 15960 df-cco 15961 df-rest 16077 df-topn 16078 df-0g 16096 df-gsum 16097 df-topgen 16098 df-pt 16099 df-prds 16102 df-xrs 16156 df-qtop 16161 df-imas 16162 df-xps 16164 df-mre 16240 df-mrc 16241 df-acs 16243 df-mgm 17236 df-sgrp 17278 df-mnd 17289 df-submnd 17330 df-mulg 17535 df-cntz 17744 df-cmn 18189 df-psmet 19732 df-xmet 19733 df-met 19734 df-bl 19735 df-mopn 19736 df-cnfld 19741 df-top 20693 df-topon 20710 df-topsp 20731 df-bases 20744 df-cld 20817 df-ntr 20818 df-cls 20819 df-cn 21025 df-cnp 21026 df-t1 21112 df-haus 21113 df-tx 21359 df-hmeo 21552 df-xms 22119 df-ms 22120 df-tms 22121 df-grpo 27331 df-gid 27332 df-ginv 27333 df-gdiv 27334 df-ablo 27383 df-vc 27398 df-nv 27431 df-va 27434 df-ba 27435 df-sm 27436 df-0v 27437 df-vs 27438 df-nmcv 27439 df-ims 27440 df-dip 27540 df-ph 27652

This theorem is referenced by: ajmoi 27698

W3C validator