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	$⊢ \underline{Ⅎ} x A$
	Assertion	disjabrexf	$⊢ \underset{x \in A}{Disj} B \to \underset{y \in \{z \| \exists x \in A z = B\}}{Disj} y$

Proof

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

Metamath Proof Explorer

Theorem disjabrexf

Proof