Metamath Proof Explorer

Theorem fvcofneq

Description: The values of two function compositions are equal if the values of the composed functions are pairwise equal. (Contributed by AV, 26-Jan-2019)

Ref Expression
Assertion fvcofneq 
|- ( ( G Fn A /\ K Fn B ) -> ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( G Fn A /\ K Fn B ) -> G Fn A )
2 elinel1 
 |-  ( X e. ( A i^i B ) -> X e. A )
3 2 3ad2ant1 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> X e. A )
4 fvco2 
 |-  ( ( G Fn A /\ X e. A ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
5 1 3 4 syl2an 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( ( F o. G ) ` X ) = ( F ` ( G ` X ) ) )
6 simpr 
 |-  ( ( G Fn A /\ K Fn B ) -> K Fn B )
7 elinel2 
 |-  ( X e. ( A i^i B ) -> X e. B )
8 7 3ad2ant1 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> X e. B )
9 fvco2 
 |-  ( ( K Fn B /\ X e. B ) -> ( ( H o. K ) ` X ) = ( H ` ( K ` X ) ) )
10 6 8 9 syl2an 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( ( H o. K ) ` X ) = ( H ` ( K ` X ) ) )
11 fveq2 
 |-  ( ( K ` X ) = ( G ` X ) -> ( H ` ( K ` X ) ) = ( H ` ( G ` X ) ) )
12 11 eqcoms 
 |-  ( ( G ` X ) = ( K ` X ) -> ( H ` ( K ` X ) ) = ( H ` ( G ` X ) ) )
13 12 3ad2ant2 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( H ` ( K ` X ) ) = ( H ` ( G ` X ) ) )
14 13 adantl 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( H ` ( K ` X ) ) = ( H ` ( G ` X ) ) )
15 id 
 |-  ( G Fn A -> G Fn A )
16 fnfvelrn 
 |-  ( ( G Fn A /\ X e. A ) -> ( G ` X ) e. ran G )
17 15 2 16 syl2anr 
 |-  ( ( X e. ( A i^i B ) /\ G Fn A ) -> ( G ` X ) e. ran G )
18 17 ex 
 |-  ( X e. ( A i^i B ) -> ( G Fn A -> ( G ` X ) e. ran G ) )
19 id 
 |-  ( K Fn B -> K Fn B )
20 fnfvelrn 
 |-  ( ( K Fn B /\ X e. B ) -> ( K ` X ) e. ran K )
21 19 7 20 syl2anr 
 |-  ( ( X e. ( A i^i B ) /\ K Fn B ) -> ( K ` X ) e. ran K )
22 21 ex 
 |-  ( X e. ( A i^i B ) -> ( K Fn B -> ( K ` X ) e. ran K ) )
23 18 22 anim12d 
 |-  ( X e. ( A i^i B ) -> ( ( G Fn A /\ K Fn B ) -> ( ( G ` X ) e. ran G /\ ( K ` X ) e. ran K ) ) )
24 eleq1 
 |-  ( ( K ` X ) = ( G ` X ) -> ( ( K ` X ) e. ran K <-> ( G ` X ) e. ran K ) )
25 24 eqcoms 
 |-  ( ( G ` X ) = ( K ` X ) -> ( ( K ` X ) e. ran K <-> ( G ` X ) e. ran K ) )
26 25 anbi2d 
 |-  ( ( G ` X ) = ( K ` X ) -> ( ( ( G ` X ) e. ran G /\ ( K ` X ) e. ran K ) <-> ( ( G ` X ) e. ran G /\ ( G ` X ) e. ran K ) ) )
27 elin 
 |-  ( ( G ` X ) e. ( ran G i^i ran K ) <-> ( ( G ` X ) e. ran G /\ ( G ` X ) e. ran K ) )
28 27 biimpri 
 |-  ( ( ( G ` X ) e. ran G /\ ( G ` X ) e. ran K ) -> ( G ` X ) e. ( ran G i^i ran K ) )
29 26 28 syl6bi 
 |-  ( ( G ` X ) = ( K ` X ) -> ( ( ( G ` X ) e. ran G /\ ( K ` X ) e. ran K ) -> ( G ` X ) e. ( ran G i^i ran K ) ) )
30 23 29 sylan9 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) ) -> ( ( G Fn A /\ K Fn B ) -> ( G ` X ) e. ( ran G i^i ran K ) ) )
31 fveq2 
 |-  ( x = ( G ` X ) -> ( F ` x ) = ( F ` ( G ` X ) ) )
32 fveq2 
 |-  ( x = ( G ` X ) -> ( H ` x ) = ( H ` ( G ` X ) ) )
33 31 32 eqeq12d 
 |-  ( x = ( G ` X ) -> ( ( F ` x ) = ( H ` x ) <-> ( F ` ( G ` X ) ) = ( H ` ( G ` X ) ) ) )
34 33 rspcva 
 |-  ( ( ( G ` X ) e. ( ran G i^i ran K ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( F ` ( G ` X ) ) = ( H ` ( G ` X ) ) )
35 34 eqcomd 
 |-  ( ( ( G ` X ) e. ( ran G i^i ran K ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) )
36 35 ex 
 |-  ( ( G ` X ) e. ( ran G i^i ran K ) -> ( A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) ) )
37 30 36 syl6 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) ) -> ( ( G Fn A /\ K Fn B ) -> ( A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) ) ) )
38 37 com23 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) ) -> ( A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) -> ( ( G Fn A /\ K Fn B ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) ) ) )
39 38 3impia 
 |-  ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( ( G Fn A /\ K Fn B ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) ) )
40 39 impcom 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( H ` ( G ` X ) ) = ( F ` ( G ` X ) ) )
41 10 14 40 3eqtrrd 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( F ` ( G ` X ) ) = ( ( H o. K ) ` X ) )
42 5 41 eqtrd 
 |-  ( ( ( G Fn A /\ K Fn B ) /\ ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) )
43 42 ex 
 |-  ( ( G Fn A /\ K Fn B ) -> ( ( X e. ( A i^i B ) /\ ( G ` X ) = ( K ` X ) /\ A. x e. ( ran G i^i ran K ) ( F ` x ) = ( H ` x ) ) -> ( ( F o. G ) ` X ) = ( ( H o. K ) ` X ) ) )