Metamath Proof Explorer

Theorem actfunsnrndisj

Description: The action F of extending function from B to C with new values at point I yields different functions. (Contributed by Thierry Arnoux, 9-Dec-2021)

Ref Expression
Hypotheses actfunsn.1 
|- ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )
actfunsn.2 
|- ( ph -> C e. _V )
actfunsn.3 
|- ( ph -> I e. V )
actfunsn.4 
|- ( ph -> -. I e. B )
actfunsn.5 
|- F = ( x e. A |-> ( x u. { <. I , k >. } ) )
Assertion actfunsnrndisj 
|- ( ph -> Disj_ k e. C ran F )

Proof

Step Hyp Ref Expression
1 actfunsn.1 
 |-  ( ( ph /\ k e. C ) -> A C_ ( C ^m B ) )
2 actfunsn.2 
 |-  ( ph -> C e. _V )
3 actfunsn.3 
 |-  ( ph -> I e. V )
4 actfunsn.4 
 |-  ( ph -> -. I e. B )
5 actfunsn.5 
 |-  F = ( x e. A |-> ( x u. { <. I , k >. } ) )
6 simpr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) /\ f = ( z u. { <. I , k >. } ) ) -> f = ( z u. { <. I , k >. } ) )
7 6 fveq1d 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) /\ f = ( z u. { <. I , k >. } ) ) -> ( f ` I ) = ( ( z u. { <. I , k >. } ) ` I ) )
8 1 ad2antrr 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> A C_ ( C ^m B ) )
9 simpr 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> z e. A )
10 8 9 sseldd 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> z e. ( C ^m B ) )
11 elmapfn 
 |-  ( z e. ( C ^m B ) -> z Fn B )
12 10 11 syl 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> z Fn B )
13 3 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> I e. V )
14 simpllr 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> k e. C )
15 fnsng 
 |-  ( ( I e. V /\ k e. C ) -> { <. I , k >. } Fn { I } )
16 13 14 15 syl2anc 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> { <. I , k >. } Fn { I } )
17 disjsn 
 |-  ( ( B i^i { I } ) = (/) <-> -. I e. B )
18 4 17 sylibr 
 |-  ( ph -> ( B i^i { I } ) = (/) )
19 18 ad3antrrr 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> ( B i^i { I } ) = (/) )
20 snidg 
 |-  ( I e. V -> I e. { I } )
21 13 20 syl 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> I e. { I } )
22 fvun2 
 |-  ( ( z Fn B /\ { <. I , k >. } Fn { I } /\ ( ( B i^i { I } ) = (/) /\ I e. { I } ) ) -> ( ( z u. { <. I , k >. } ) ` I ) = ( { <. I , k >. } ` I ) )
23 12 16 19 21 22 syl112anc 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> ( ( z u. { <. I , k >. } ) ` I ) = ( { <. I , k >. } ` I ) )
24 fvsng 
 |-  ( ( I e. V /\ k e. C ) -> ( { <. I , k >. } ` I ) = k )
25 13 14 24 syl2anc 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> ( { <. I , k >. } ` I ) = k )
26 23 25 eqtrd 
 |-  ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) -> ( ( z u. { <. I , k >. } ) ` I ) = k )
27 26 adantr 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) /\ f = ( z u. { <. I , k >. } ) ) -> ( ( z u. { <. I , k >. } ) ` I ) = k )
28 7 27 eqtrd 
 |-  ( ( ( ( ( ph /\ k e. C ) /\ f e. ran F ) /\ z e. A ) /\ f = ( z u. { <. I , k >. } ) ) -> ( f ` I ) = k )
29 simpr 
 |-  ( ( ( ph /\ k e. C ) /\ f e. ran F ) -> f e. ran F )
30 uneq1 
 |-  ( x = z -> ( x u. { <. I , k >. } ) = ( z u. { <. I , k >. } ) )
31 30 cbvmptv 
 |-  ( x e. A |-> ( x u. { <. I , k >. } ) ) = ( z e. A |-> ( z u. { <. I , k >. } ) )
32 5 31 eqtri 
 |-  F = ( z e. A |-> ( z u. { <. I , k >. } ) )
33 vex 
 |-  z e. _V
34 snex 
 |-  { <. I , k >. } e. _V
35 33 34 unex 
 |-  ( z u. { <. I , k >. } ) e. _V
36 32 35 elrnmpti 
 |-  ( f e. ran F <-> E. z e. A f = ( z u. { <. I , k >. } ) )
37 29 36 sylib 
 |-  ( ( ( ph /\ k e. C ) /\ f e. ran F ) -> E. z e. A f = ( z u. { <. I , k >. } ) )
38 28 37 r19.29a 
 |-  ( ( ( ph /\ k e. C ) /\ f e. ran F ) -> ( f ` I ) = k )
39 38 ralrimiva 
 |-  ( ( ph /\ k e. C ) -> A. f e. ran F ( f ` I ) = k )
40 39 ralrimiva 
 |-  ( ph -> A. k e. C A. f e. ran F ( f ` I ) = k )
41 invdisj 
 |-  ( A. k e. C A. f e. ran F ( f ` I ) = k -> Disj_ k e. C ran F )
42 40 41 syl 
 |-  ( ph -> Disj_ k e. C ran F )