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 A B Disj y z | x A z = B y

Proof

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