Theorem phoeqi

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

	Ref	Expression
Hypotheses	ip2eqi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
	ip2eqi.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
	ip2eqi.u	⊢ 𝑈 ∈ CPreHilOLD
Assertion	phoeqi	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ 𝑆 = 𝑇 ) )

Proof

Step	Hyp	Ref	Expression
1		ip2eqi.1	⊢ 𝑋 = ( BaseSet ‘ 𝑈 )
2		ip2eqi.7	⊢ 𝑃 = ( ·𝑖OLD ‘ 𝑈 )
3		ip2eqi.u	⊢ 𝑈 ∈ CPreHilOLD
4		ralcom	⊢ ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) )
5		ffvelcdm	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑆 ‘ 𝑦 ) ∈ 𝑋 )
6		ffvelcdm	⊢ ( ( 𝑇 : 𝑌 ⟶ 𝑋 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑇 ‘ 𝑦 ) ∈ 𝑋 )
7	1 2 3	ip2eqi	⊢ ( ( ( 𝑆 ‘ 𝑦 ) ∈ 𝑋 ∧ ( 𝑇 ‘ 𝑦 ) ∈ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
8	5 6 7	syl2an	⊢ ( ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ∧ ( 𝑇 : 𝑌 ⟶ 𝑋 ∧ 𝑦 ∈ 𝑌 ) ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
9	8	anandirs	⊢ ( ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) ∧ 𝑦 ∈ 𝑌 ) → ( ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
10	9	ralbidva	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
11		ffn	⊢ ( 𝑆 : 𝑌 ⟶ 𝑋 → 𝑆 Fn 𝑌 )
12		ffn	⊢ ( 𝑇 : 𝑌 ⟶ 𝑋 → 𝑇 Fn 𝑌 )
13		eqfnfv	⊢ ( ( 𝑆 Fn 𝑌 ∧ 𝑇 Fn 𝑌 ) → ( 𝑆 = 𝑇 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
14	11 12 13	syl2an	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) → ( 𝑆 = 𝑇 ↔ ∀ 𝑦 ∈ 𝑌 ( 𝑆 ‘ 𝑦 ) = ( 𝑇 ‘ 𝑦 ) ) )
15	10 14	bitr4d	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑦 ∈ 𝑌 ∀ 𝑥 ∈ 𝑋 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ 𝑆 = 𝑇 ) )
16	4 15	bitrid	⊢ ( ( 𝑆 : 𝑌 ⟶ 𝑋 ∧ 𝑇 : 𝑌 ⟶ 𝑋 ) → ( ∀ 𝑥 ∈ 𝑋 ∀ 𝑦 ∈ 𝑌 ( 𝑥 𝑃 ( 𝑆 ‘ 𝑦 ) ) = ( 𝑥 𝑃 ( 𝑇 ‘ 𝑦 ) ) ↔ 𝑆 = 𝑇 ) )