Metamath Proof Explorer

Theorem disjabrexf

Description: Rewriting a disjoint collection into a partition of its image set. (Contributed by Thierry Arnoux, 30-Dec-2016) (Revised by Thierry Arnoux, 9-Mar-2017)

Ref Expression
Hypothesis disjabrexf.1 
|- F/_ x A
Assertion disjabrexf 
|- ( Disj_ x e. A B -> Disj_ y e. { z | E. x e. A z = B } y )

Proof

Step Hyp Ref Expression
1 disjabrexf.1 
 |-  F/_ x A
2 nfdisj1 
 |-  F/ x Disj_ x e. A B
3 nfcv 
 |-  F/_ x y
4 1 nfcri 
 |-  F/ x i e. A
5 nfcsb1v 
 |-  F/_ x [_ i / x ]_ B
6 5 nfcri 
 |-  F/ x j e. [_ i / x ]_ B
7 4 6 nfan 
 |-  F/ x ( i e. A /\ j e. [_ i / x ]_ B )
8 7 nfab 
 |-  F/_ x { i | ( i e. A /\ j e. [_ i / x ]_ B ) }
9 8 nfuni 
 |-  F/_ x U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) }
10 9 nfcsb1 
 |-  F/_ x [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B
11 10 nfeq1 
 |-  F/ x [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y
12 3 11 nfralw 
 |-  F/ x A. j e. y [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y
13 eqeq2 
 |-  ( y = B -> ( [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y <-> [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = B ) )
14 13 raleqbi1dv 
 |-  ( y = B -> ( A. j e. y [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y <-> A. j e. B [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = B ) )
15 vex 
 |-  y e. _V
16 15 a1i 
 |-  ( Disj_ x e. A B -> y e. _V )
17 simplll 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> Disj_ x e. A B )
18 simpllr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> x e. A )
19 simprl 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> i e. A )
20 simplr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> j e. B )
21 simprr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> j e. [_ i / x ]_ B )
22 csbeq1a 
 |-  ( x = i -> B = [_ i / x ]_ B )
23 1 5 22 disjif2 
 |-  ( ( Disj_ x e. A B /\ ( x e. A /\ i e. A ) /\ ( j e. B /\ j e. [_ i / x ]_ B ) ) -> x = i )
24 17 18 19 20 21 23 syl122anc 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ ( i e. A /\ j e. [_ i / x ]_ B ) ) -> x = i )
25 simpr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> x = i )
26 simpllr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> x e. A )
27 25 26 eqeltrrd 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> i e. A )
28 simplr 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> j e. B )
29 22 eleq2d 
 |-  ( x = i -> ( j e. B <-> j e. [_ i / x ]_ B ) )
30 25 29 syl 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> ( j e. B <-> j e. [_ i / x ]_ B ) )
31 28 30 mpbid 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> j e. [_ i / x ]_ B )
32 27 31 jca 
 |-  ( ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) /\ x = i ) -> ( i e. A /\ j e. [_ i / x ]_ B ) )
33 24 32 impbida 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> ( ( i e. A /\ j e. [_ i / x ]_ B ) <-> x = i ) )
34 equcom 
 |-  ( x = i <-> i = x )
35 33 34 bitrdi 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> ( ( i e. A /\ j e. [_ i / x ]_ B ) <-> i = x ) )
36 35 abbidv 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = { i | i = x } )
37 df-sn 
 |-  { x } = { i | i = x }
38 36 37 eqtr4di 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = { x } )
39 38 unieqd 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = U. { x } )
40 vex 
 |-  x e. _V
41 40 unisn 
 |-  U. { x } = x
42 39 41 eqtrdi 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = x )
43 csbeq1 
 |-  ( U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = x -> [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = [_ x / x ]_ B )
44 csbid 
 |-  [_ x / x ]_ B = B
45 43 44 eqtrdi 
 |-  ( U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } = x -> [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = B )
46 42 45 syl 
 |-  ( ( ( Disj_ x e. A B /\ x e. A ) /\ j e. B ) -> [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = B )
47 46 ralrimiva 
 |-  ( ( Disj_ x e. A B /\ x e. A ) -> A. j e. B [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = B )
48 2 12 14 16 47 elabreximd 
 |-  ( ( Disj_ x e. A B /\ y e. { z | E. x e. A z = B } ) -> A. j e. y [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y )
49 48 ralrimiva 
 |-  ( Disj_ x e. A B -> A. y e. { z | E. x e. A z = B } A. j e. y [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y )
50 invdisj 
 |-  ( A. y e. { z | E. x e. A z = B } A. j e. y [_ U. { i | ( i e. A /\ j e. [_ i / x ]_ B ) } / x ]_ B = y -> Disj_ y e. { z | E. x e. A z = B } y )
51 49 50 syl 
 |-  ( Disj_ x e. A B -> Disj_ y e. { z | E. x e. A z = B } y )