Theorem disjabrex 32568

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 5105	. . . 4 ⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
2		nfcv 2899	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfv 1914	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑖 ∈ 𝐴
4		nfcsb1v 3903	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
5	4	nfcri 2891	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵
6	3, 5	nfan 1899	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
7	6	nfab 2905	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
8	7	nfuni 4895	. . . . . . 7 ⊢ Ⅎ𝑥∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
9	8	nfcsb1 3902	. . . . . 6 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵
10	9	nfeq1 2915	. . . . 5 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
11	2, 10	nfralw 3295	. . . 4 ⊢ Ⅎ𝑥∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
12		eqeq2 2748	. . . . 5 ⊢ (𝑦 = 𝐵 → (⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
13	12	raleqbi1dv 3321	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
14		vex 3468	. . . . 5 ⊢ 𝑦 ∈ V
15	14	a1i 11	. . . 4 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ V)
16		simplll 774	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → Disj 𝑥 ∈ 𝐴 𝐵)
17		simpllr 775	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 ∈ 𝐴)
18		simprl 770	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑖 ∈ 𝐴)
19		simplr 768	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ 𝐵)
20		simprr 772	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
21		csbeq1a 3893	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
22	4, 21	disjif 32564	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
23	16, 17, 18, 19, 20, 22	syl122anc 1381	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
24		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖)
25		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 ∈ 𝐴)
26	24, 25	eqeltrrd 2836	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐴)
27		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ 𝐵)
28	21	eleq2d 2821	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
29	24, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
30	27, 29	mpbid 232	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
31	26, 30	jca 511	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
32	23, 31	impbida 800	. . . . . . . . . . 11 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑥 = 𝑖))
33		equcom 2018	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 ↔ 𝑖 = 𝑥)
34	32, 33	bitrdi 287	. . . . . . . . . 10 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑖 = 𝑥))
35	34	abbidv 2802	. . . . . . . . 9 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑖 ∣ 𝑖 = 𝑥})
36		df-sn 4607	. . . . . . . . 9 ⊢ {𝑥} = {𝑖 ∣ 𝑖 = 𝑥}
37	35, 36	eqtr4di 2789	. . . . . . . 8 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑥})
38	37	unieqd 4901	. . . . . . 7 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = ∪ {𝑥})
39		unisnv 4908	. . . . . . 7 ⊢ ∪ {𝑥} = 𝑥
40	38, 39	eqtrdi 2787	. . . . . 6 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥)
41		csbeq1 3882	. . . . . . 7 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵)
42		csbid 3892	. . . . . . 7 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
43	41, 42	eqtrdi 2787	. . . . . 6 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
44	40, 43	syl 17	. . . . 5 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
45	44	ralrimiva 3133	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
46	1, 11, 13, 15, 45	elabreximd 32496	. . 3 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
47	46	ralrimiva 3133	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
48		invdisj 5110	. 2 ⊢ (∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
49	47, 48	syl 17	1 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1540   ∈ wcel 2109  {cab 2714  ∀wral 3052  ∃wrex 3061  Vcvv 3464  ⦋csb 3879  {csn 4606  ∪ cuni 4888  Disj wdisj 5091

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-mo 2540  df-clab 2715  df-cleq 2728  df-clel 2810  df-nfc 2886  df-ne 2934  df-ral 3053  df-rex 3062  df-rmo 3364  df-rab 3421  df-v 3466  df-sbc 3771  df-csb 3880  df-dif 3934  df-un 3936  df-in 3938  df-ss 3948  df-nul 4314  df-sn 4607  df-pr 4609  df-uni 4889  df-disj 5092

This theorem is referenced by:  disjrnmpt  32571