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

Proof

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