Theorem disjabrex 32596

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 5123	. . . 4 ⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
2		nfcv 2904	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfv 1913	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑖 ∈ 𝐴
4		nfcsb1v 3922	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
5	4	nfcri 2896	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵
6	3, 5	nfan 1898	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
7	6	nfab 2910	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
8	7	nfuni 4913	. . . . . . 7 ⊢ Ⅎ𝑥∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
9	8	nfcsb1 3921	. . . . . 6 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵
10	9	nfeq1 2920	. . . . 5 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
11	2, 10	nfralw 3310	. . . 4 ⊢ Ⅎ𝑥∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
12		eqeq2 2748	. . . . 5 ⊢ (𝑦 = 𝐵 → (⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
13	12	raleqbi1dv 3337	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
14		vex 3483	. . . . 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 3912	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
22	4, 21	disjif 32592	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
23	16, 17, 18, 19, 20, 22	syl122anc 1380	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
24		simpr 484	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖)
25		simpllr 775	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 ∈ 𝐴)
26	24, 25	eqeltrrd 2841	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐴)
27		simplr 768	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ 𝐵)
28	21	eleq2d 2826	. . . . . . . . . . . . . . 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 2016	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 ↔ 𝑖 = 𝑥)
34	32, 33	bitrdi 287	. . . . . . . . . 10 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑖 = 𝑥))
35	34	abbidv 2807	. . . . . . . . 9 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑖 ∣ 𝑖 = 𝑥})
36		df-sn 4626	. . . . . . . . 9 ⊢ {𝑥} = {𝑖 ∣ 𝑖 = 𝑥}
37	35, 36	eqtr4di 2794	. . . . . . . 8 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑥})
38	37	unieqd 4919	. . . . . . 7 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = ∪ {𝑥})
39		unisnv 4926	. . . . . . 7 ⊢ ∪ {𝑥} = 𝑥
40	38, 39	eqtrdi 2792	. . . . . 6 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥)
41		csbeq1 3901	. . . . . . 7 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵)
42		csbid 3911	. . . . . . 7 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
43	41, 42	eqtrdi 2792	. . . . . 6 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
44	40, 43	syl 17	. . . . 5 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
45	44	ralrimiva 3145	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
46	1, 11, 13, 15, 45	elabreximd 32530	. . 3 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
47	46	ralrimiva 3145	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
48		invdisj 5128	. 2 ⊢ (∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
49	47, 48	syl 17	1 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   = wceq 1539   ∈ wcel 2107  {cab 2713  ∀wral 3060  ∃wrex 3069  Vcvv 3479  ⦋csb 3898  {csn 4625  ∪ cuni 4906  Disj wdisj 5109

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-10 2140  ax-11 2156  ax-12 2176  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-nf 1783  df-sb 2064  df-mo 2539  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-ral 3061  df-rex 3070  df-rmo 3379  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-nul 4333  df-sn 4626  df-pr 4628  df-uni 4907  df-disj 5110

This theorem is referenced by:  disjrnmpt  32599