disjabrex

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

		Ref	Expression
	Assertion	disjabrex	$⊢ \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		nfdisj1	$⊢ Ⅎ x \underset{x \in A}{Disj} B$
2		nfcv	$⊢ \underline{Ⅎ} x y$
3		nfv	$⊢ Ⅎ x i \in A$
4		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ i / x ⦌ B$
5	4	nfcri	$⊢ Ⅎ x j \in ⦋ i / x ⦌ B$
6	3 5	nfan	$⊢ Ⅎ x (i \in A \land j \in ⦋ i / x ⦌ B)$
7	6	nfab	$⊢ \underline{Ⅎ} x \{i \| (i \in A \land j \in ⦋ i / x ⦌ B)\}$
8	7	nfuni	$⊢ \underline{Ⅎ} x ⋃ \{i \| (i \in A \land j \in ⦋ i / x ⦌ B)\}$
9	8	nfcsb1	$⊢ \underline{Ⅎ} x ⦋ ⋃ \{i \| (i \in A \land j \in ⦋ i / x ⦌ B)\} / x ⦌ B$
10	9	nfeq1	$⊢ Ⅎ x ⦋ ⋃ \{i \| (i \in A \land j \in ⦋ i / x ⦌ B)\} / x ⦌ B = y$
11	2 10	nfralw	$⊢ Ⅎ x \forall j \in y ⦋ ⋃ \{i \| (i \in A \land j \in ⦋ i / x ⦌ B)\} / x ⦌ B = y$
12		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)$
13	12	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)$
14		vex	$⊢ y \in V$
15	14	a1i	$⊢ \underset{x \in A}{Disj} B \to y \in V$
16		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$
17		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$
18		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$
19		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$
20		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$
21		csbeq1a	$⊢ x = i \to B = ⦋ i / x ⦌ B$
22	4 21	disjif	$⊢ (\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$
23	16 17 18 19 20 22	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$
24		simpr	$⊢ (((\underset{x \in A}{Disj} B \land x \in A) \land j \in B) \land x = i) \to x = i$
25		simpllr	$⊢ (((\underset{x \in A}{Disj} B \land x \in A) \land j \in B) \land x = i) \to x \in A$
26	24 25	eqeltrrd	$⊢ (((\underset{x \in A}{Disj} B \land x \in A) \land j \in B) \land x = i) \to i \in A$
27		simplr	$⊢ (((\underset{x \in A}{Disj} B \land x \in A) \land j \in B) \land x = i) \to j \in B$
28	21	eleq2d	$⊢ x = i \to (j \in B \leftrightarrow j \in ⦋ i / x ⦌ B)$
29	24 28	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)$
30	27 29	mpbid	$⊢ (((\underset{x \in A}{Disj} B \land x \in A) \land j \in B) \land x = i) \to j \in ⦋ i / x ⦌ B$
31	26 30	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)$
32	23 31	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)$
33		equcom	$⊢ x = i \leftrightarrow i = x$
34	32 33	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)$
35	34	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\}$
36		df-sn	$⊢ \{x\} = \{i \| i = x\}$
37	35 36	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\}$
38	37	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\}$
39		unisnv	$⊢ ⋃ \{x\} = x$
40	38 39	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$
41		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$
42		csbid	$⊢ ⦋ x / x ⦌ B = B$
43	41 42	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$
44	40 43	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$
45	44	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$
46	1 11 13 15 45	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$
47	46	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$
48		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$
49	47 48	syl	$⊢ \underset{x \in A}{Disj} B \to \underset{y \in \{z \| \exists x \in A z = B\}}{Disj} y$

Metamath Proof Explorer

Theorem disjabrex

Proof