This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 = ( .iOLD ` U )
ip2eqi.u 
|- U e. CPreHilOLD
Assertion phoeqi 
|- ( ( S : Y --> X /\ T : Y --> X ) -> ( A. x e. X A. y e. 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 = ( .iOLD ` U )
3 ip2eqi.u 
 |-  U e. CPreHilOLD
4 ralcom 
 |-  ( A. x e. X A. y e. Y ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) )
5 ffvelcdm 
 |-  ( ( S : Y --> X /\ y e. Y ) -> ( S ` y ) e. X )
6 ffvelcdm 
 |-  ( ( T : Y --> X /\ y e. Y ) -> ( T ` y ) e. X )
7 1 2 3 ip2eqi 
 |-  ( ( ( S ` y ) e. X /\ ( T ` y ) e. X ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
8 5 6 7 syl2an 
 |-  ( ( ( S : Y --> X /\ y e. Y ) /\ ( T : Y --> X /\ y e. Y ) ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
9 8 anandirs 
 |-  ( ( ( S : Y --> X /\ T : Y --> X ) /\ y e. Y ) -> ( A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> ( S ` y ) = ( T ` y ) ) )
10 9 ralbidva 
 |-  ( ( S : Y --> X /\ T : Y --> X ) -> ( A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> A. y e. 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 <-> A. y e. Y ( S ` y ) = ( T ` y ) ) )
14 11 12 13 syl2an 
 |-  ( ( S : Y --> X /\ T : Y --> X ) -> ( S = T <-> A. y e. Y ( S ` y ) = ( T ` y ) ) )
15 10 14 bitr4d 
 |-  ( ( S : Y --> X /\ T : Y --> X ) -> ( A. y e. Y A. x e. X ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> S = T ) )
16 4 15 bitrid 
 |-  ( ( S : Y --> X /\ T : Y --> X ) -> ( A. x e. X A. y e. Y ( x P ( S ` y ) ) = ( x P ( T ` y ) ) <-> S = T ) )