Metamath Proof Explorer

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 ⊢ X = BaseSet ⁡ U
ip2eqi.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
ip2eqi.u ⊢ U ∈ CPreHil OLD
Assertion phoeqi ⊢ S : Y ⟶ X ∧ T : Y ⟶ X → ∀ x ∈ X ∀ y ∈ Y x P S ⁡ y = x P T ⁡ y ↔ S = T

Proof

Step Hyp Ref Expression
1 ip2eqi.1 ⊢ X = BaseSet ⁡ U
2 ip2eqi.7 ⊢ P = ⋅ 𝑖OLD ⁡ U
3 ip2eqi.u ⊢ U ∈ CPreHil OLD
4 ralcom ⊢ ∀ x ∈ X ∀ y ∈ Y x P S ⁡ y = x P T ⁡ y ↔ ∀ y ∈ Y ∀ x ∈ X x P S ⁡ y = x P T ⁡ y
5 ffvelcdm ⊢ S : Y ⟶ X ∧ y ∈ Y → S ⁡ y ∈ X
6 ffvelcdm ⊢ T : Y ⟶ X ∧ y ∈ Y → T ⁡ y ∈ X
7 1 2 3 ip2eqi ⊢ S ⁡ y ∈ X ∧ T ⁡ y ∈ X → ∀ x ∈ X x P S ⁡ y = x P T ⁡ y ↔ S ⁡ y = T ⁡ y
8 5 6 7 syl2an ⊢ S : Y ⟶ X ∧ y ∈ Y ∧ T : Y ⟶ X ∧ y ∈ Y → ∀ x ∈ X x P S ⁡ y = x P T ⁡ y ↔ S ⁡ y = T ⁡ y
9 8 anandirs ⊢ S : Y ⟶ X ∧ T : Y ⟶ X ∧ y ∈ Y → ∀ x ∈ X x P S ⁡ y = x P T ⁡ y ↔ S ⁡ y = T ⁡ y
10 9 ralbidva ⊢ S : Y ⟶ X ∧ T : Y ⟶ X → ∀ y ∈ Y ∀ x ∈ X x P S ⁡ y = x P T ⁡ y ↔ ∀ y ∈ Y S ⁡ y = T ⁡ y
11 ffn ⊢ S : Y ⟶ X → S Fn Y
12 ffn ⊢ T : Y ⟶ X → T Fn Y
13 eqfnfv ⊢ S Fn Y ∧ T Fn Y → S = T ↔ ∀ y ∈ Y S ⁡ y = T ⁡ y
14 11 12 13 syl2an ⊢ S : Y ⟶ X ∧ T : Y ⟶ X → S = T ↔ ∀ y ∈ Y S ⁡ y = T ⁡ y
15 10 14 bitr4d ⊢ S : Y ⟶ X ∧ T : Y ⟶ X → ∀ y ∈ Y ∀ x ∈ X x P S ⁡ y = x P T ⁡ y ↔ S = T
16 4 15 bitrid ⊢ S : Y ⟶ X ∧ T : Y ⟶ X → ∀ x ∈ X ∀ y ∈ Y x P S ⁡ y = x P T ⁡ y ↔ S = T