Metamath Proof Explorer

Theorem disjabrex

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

Ref Expression
Assertion disjabrex 
|- ( Disj_ x e. A B -> Disj_ y e. { z | E. x e. A z = B } y )

Proof

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