Theorem disjabrex 32741

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

Assertion

Ref	Expression
disjabrex	⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)

Distinct variable groups:   𝑥,𝑦,𝑧,𝐴   𝑦,𝐵,𝑧

Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem disjabrex

Dummy variables 𝑖 𝑗 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		nfdisj1 5078	. . . 4 ⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
2		nfcv 2923	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfv 1933	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑖 ∈ 𝐴
4		nfcsb1v 3874	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
5	4	nfcri 2915	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵
6	3, 5	nfan 1918	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
7	6	nfab 2929	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
8	7	nfuni 4869	. . . . . . 7 ⊢ Ⅎ𝑥∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
9	8	nfcsb1 3873	. . . . . 6 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵
10	9	nfeq1 2938	. . . . 5 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
11	2, 10	nfralw 3308	. . . 4 ⊢ Ⅎ𝑥∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
12		eqeq2 2773	. . . . 5 ⊢ (𝑦 = 𝐵 → (⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
13	12	raleqbi1dv 3329	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
14		vex 3457	. . . . 5 ⊢ 𝑦 ∈ V
15	14	a1i 11	. . . 4 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ V)
16		simplll 784	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → Disj 𝑥 ∈ 𝐴 𝐵)
17		simpllr 785	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 ∈ 𝐴)
18		simprl 780	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑖 ∈ 𝐴)
19		simplr 778	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ 𝐵)
20		simprr 782	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
21		csbeq1a 3864	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
22	4, 21	disjif 32737	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
23	16, 17, 18, 19, 20, 22	syl122anc 1397	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
24		simpr 488	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖)
25		simpllr 785	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 ∈ 𝐴)
26	24, 25	eqeltrrd 2862	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐴)
27		simplr 778	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ 𝐵)
28	21	eleq2d 2847	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
29	24, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
30	27, 29	mpbid 234	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
31	26, 30	jca 519	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
32	23, 31	impbida 810	. . . . . . . . . . 11 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑥 = 𝑖))
33		equcom 2037	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 ↔ 𝑖 = 𝑥)
34	32, 33	bitrdi 289	. . . . . . . . . 10 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑖 = 𝑥))
35	34	abbidv 2827	. . . . . . . . 9 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑖 ∣ 𝑖 = 𝑥})
36		df-sn 4580	. . . . . . . . 9 ⊢ {𝑥} = {𝑖 ∣ 𝑖 = 𝑥}
37	35, 36	eqtr4di 2814	. . . . . . . 8 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑥})
38	37	unieqd 4875	. . . . . . 7 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = ∪ {𝑥})
39		unisnv 4882	. . . . . . 7 ⊢ ∪ {𝑥} = 𝑥
40	38, 39	eqtrdi 2812	. . . . . 6 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥)
41		csbeq1 3853	. . . . . . 7 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵)
42		csbid 3863	. . . . . . 7 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
43	41, 42	eqtrdi 2812	. . . . . 6 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
44	40, 43	syl 17	. . . . 5 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
45	44	ralrimiva 3153	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
46	1, 11, 13, 15, 45	elabreximd 32668	. . 3 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
47	46	ralrimiva 3153	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
48		invdisj 5083	. 2 ⊢ (∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
49	47, 48	syl 17	1 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)

Syntax hints:   → wi 4   ↔ wb 208   ∧ wa 399   = wceq 1559   ∈ wcel 2141  {cab 2739  ∀wral 3075  ∃wrex 3085  Vcvv 3453  ⦋csb 3850  {csn 4579  ∪ cuni 4862  Disj wdisj 5064

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-nf 1803  df-sb 2090  df-mo 2565  df-clab 2740  df-cleq 2753  df-clel 2836  df-nfc 2910  df-ne 2957  df-ral 3076  df-rex 3086  df-rmo 3366  df-rab 3414  df-v 3455  df-sbc 3743  df-csb 3851  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-sn 4580  df-pr 4582  df-uni 4863  df-disj 5065

This theorem is referenced by:  disjrnmpt  32744