Metamath Proof Explorer

Theorem disjpreima

Description: A preimage of a disjoint set is disjoint. (Contributed by Thierry Arnoux, 7-Feb-2017)

Ref Expression
Assertion disjpreima 
|- ( ( Fun F /\ Disj_ x e. A B ) -> Disj_ x e. A ( `' F " B ) )

Proof

Step Hyp Ref Expression
1 inpreima 
 |-  ( Fun F -> ( `' F " ( [_ y / x ]_ B i^i [_ z / x ]_ B ) ) = ( ( `' F " [_ y / x ]_ B ) i^i ( `' F " [_ z / x ]_ B ) ) )
2 imaeq2 
 |-  ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) -> ( `' F " ( [_ y / x ]_ B i^i [_ z / x ]_ B ) ) = ( `' F " (/) ) )
3 ima0 
 |-  ( `' F " (/) ) = (/)
4 2 3 eqtrdi 
 |-  ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) -> ( `' F " ( [_ y / x ]_ B i^i [_ z / x ]_ B ) ) = (/) )
5 1 4 sylan9req 
 |-  ( ( Fun F /\ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) -> ( ( `' F " [_ y / x ]_ B ) i^i ( `' F " [_ z / x ]_ B ) ) = (/) )
6 5 ex 
 |-  ( Fun F -> ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) -> ( ( `' F " [_ y / x ]_ B ) i^i ( `' F " [_ z / x ]_ B ) ) = (/) ) )
7 csbima12 
 |-  [_ y / x ]_ ( `' F " B ) = ( [_ y / x ]_ `' F " [_ y / x ]_ B )
8 csbconstg 
 |-  ( y e. _V -> [_ y / x ]_ `' F = `' F )
9 8 elv 
 |-  [_ y / x ]_ `' F = `' F
10 9 imaeq1i 
 |-  ( [_ y / x ]_ `' F " [_ y / x ]_ B ) = ( `' F " [_ y / x ]_ B )
11 7 10 eqtri 
 |-  [_ y / x ]_ ( `' F " B ) = ( `' F " [_ y / x ]_ B )
12 csbima12 
 |-  [_ z / x ]_ ( `' F " B ) = ( [_ z / x ]_ `' F " [_ z / x ]_ B )
13 csbconstg 
 |-  ( z e. _V -> [_ z / x ]_ `' F = `' F )
14 13 elv 
 |-  [_ z / x ]_ `' F = `' F
15 14 imaeq1i 
 |-  ( [_ z / x ]_ `' F " [_ z / x ]_ B ) = ( `' F " [_ z / x ]_ B )
16 12 15 eqtri 
 |-  [_ z / x ]_ ( `' F " B ) = ( `' F " [_ z / x ]_ B )
17 11 16 ineq12i 
 |-  ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = ( ( `' F " [_ y / x ]_ B ) i^i ( `' F " [_ z / x ]_ B ) )
18 17 eqeq1i 
 |-  ( ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) <-> ( ( `' F " [_ y / x ]_ B ) i^i ( `' F " [_ z / x ]_ B ) ) = (/) )
19 6 18 imbitrrdi 
 |-  ( Fun F -> ( ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) -> ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) ) )
20 19 orim2d 
 |-  ( Fun F -> ( ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) -> ( y = z \/ ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) ) ) )
21 20 ralimdv 
 |-  ( Fun F -> ( A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) -> A. z e. A ( y = z \/ ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) ) ) )
22 21 ralimdv 
 |-  ( Fun F -> ( A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) -> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) ) ) )
23 disjors 
 |-  ( Disj_ x e. A B <-> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ B i^i [_ z / x ]_ B ) = (/) ) )
24 disjors 
 |-  ( Disj_ x e. A ( `' F " B ) <-> A. y e. A A. z e. A ( y = z \/ ( [_ y / x ]_ ( `' F " B ) i^i [_ z / x ]_ ( `' F " B ) ) = (/) ) )
25 22 23 24 3imtr4g 
 |-  ( Fun F -> ( Disj_ x e. A B -> Disj_ x e. A ( `' F " B ) ) )
26 25 imp 
 |-  ( ( Fun F /\ Disj_ x e. A B ) -> Disj_ x e. A ( `' F " B ) )