Theorem disjabrex 30921

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 5053	. . . 4 ⊢ Ⅎ𝑥Disj 𝑥 ∈ 𝐴 𝐵
2		nfcv 2907	. . . . 5 ⊢ Ⅎ𝑥𝑦
3		nfv 1917	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑖 ∈ 𝐴
4		nfcsb1v 3857	. . . . . . . . . . 11 ⊢ Ⅎ𝑥⦋𝑖 / 𝑥⦌𝐵
5	4	nfcri 2894	. . . . . . . . . 10 ⊢ Ⅎ𝑥 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵
6	3, 5	nfan 1902	. . . . . . . . 9 ⊢ Ⅎ𝑥(𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
7	6	nfab 2913	. . . . . . . 8 ⊢ Ⅎ𝑥{𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
8	7	nfuni 4846	. . . . . . 7 ⊢ Ⅎ𝑥∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)}
9	8	nfcsb1 3856	. . . . . 6 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵
10	9	nfeq1 2922	. . . . 5 ⊢ Ⅎ𝑥⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
11	2, 10	nfralw 3151	. . . 4 ⊢ Ⅎ𝑥∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦
12		eqeq2 2750	. . . . 5 ⊢ (𝑦 = 𝐵 → (⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
13	12	raleqbi1dv 3340	. . . 4 ⊢ (𝑦 = 𝐵 → (∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 ↔ ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵))
14		vex 3436	. . . . 5 ⊢ 𝑦 ∈ V
15	14	a1i 11	. . . 4 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → 𝑦 ∈ V)
16		simplll 772	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → Disj 𝑥 ∈ 𝐴 𝐵)
17		simpllr 773	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 ∈ 𝐴)
18		simprl 768	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑖 ∈ 𝐴)
19		simplr 766	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ 𝐵)
20		simprr 770	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
21		csbeq1a 3846	. . . . . . . . . . . . . 14 ⊢ (𝑥 = 𝑖 → 𝐵 = ⦋𝑖 / 𝑥⦌𝐵)
22	4, 21	disjif 30917	. . . . . . . . . . . . 13 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ (𝑥 ∈ 𝐴 ∧ 𝑖 ∈ 𝐴) ∧ (𝑗 ∈ 𝐵 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
23	16, 17, 18, 19, 20, 22	syl122anc 1378	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)) → 𝑥 = 𝑖)
24		simpr 485	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 = 𝑖)
25		simpllr 773	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑥 ∈ 𝐴)
26	24, 25	eqeltrrd 2840	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑖 ∈ 𝐴)
27		simplr 766	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ 𝐵)
28	21	eleq2d 2824	. . . . . . . . . . . . . . 15 ⊢ (𝑥 = 𝑖 → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
29	24, 28	syl 17	. . . . . . . . . . . . . 14 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑗 ∈ 𝐵 ↔ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
30	27, 29	mpbid 231	. . . . . . . . . . . . 13 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)
31	26, 30	jca 512	. . . . . . . . . . . 12 ⊢ ((((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) ∧ 𝑥 = 𝑖) → (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵))
32	23, 31	impbida 798	. . . . . . . . . . 11 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑥 = 𝑖))
33		equcom 2021	. . . . . . . . . . 11 ⊢ (𝑥 = 𝑖 ↔ 𝑖 = 𝑥)
34	32, 33	bitrdi 287	. . . . . . . . . 10 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ((𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵) ↔ 𝑖 = 𝑥))
35	34	abbidv 2807	. . . . . . . . 9 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑖 ∣ 𝑖 = 𝑥})
36		df-sn 4562	. . . . . . . . 9 ⊢ {𝑥} = {𝑖 ∣ 𝑖 = 𝑥}
37	35, 36	eqtr4di 2796	. . . . . . . 8 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = {𝑥})
38	37	unieqd 4853	. . . . . . 7 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = ∪ {𝑥})
39		vex 3436	. . . . . . . 8 ⊢ 𝑥 ∈ V
40	39	unisn 4861	. . . . . . 7 ⊢ ∪ {𝑥} = 𝑥
41	38, 40	eqtrdi 2794	. . . . . 6 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥)
42		csbeq1 3835	. . . . . . 7 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = ⦋𝑥 / 𝑥⦌𝐵)
43		csbid 3845	. . . . . . 7 ⊢ ⦋𝑥 / 𝑥⦌𝐵 = 𝐵
44	42, 43	eqtrdi 2794	. . . . . 6 ⊢ (∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} = 𝑥 → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
45	41, 44	syl 17	. . . . 5 ⊢ (((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) ∧ 𝑗 ∈ 𝐵) → ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
46	45	ralrimiva 3103	. . . 4 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑥 ∈ 𝐴) → ∀𝑗 ∈ 𝐵 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝐵)
47	1, 11, 13, 15, 46	elabreximd 30855	. . 3 ⊢ ((Disj 𝑥 ∈ 𝐴 𝐵 ∧ 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}) → ∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
48	47	ralrimiva 3103	. 2 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → ∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦)
49		invdisj 5058	. 2 ⊢ (∀𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}∀𝑗 ∈ 𝑦 ⦋∪ {𝑖 ∣ (𝑖 ∈ 𝐴 ∧ 𝑗 ∈ ⦋𝑖 / 𝑥⦌𝐵)} / 𝑥⦌𝐵 = 𝑦 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)
50	48, 49	syl 17	1 ⊢ (Disj 𝑥 ∈ 𝐴 𝐵 → Disj 𝑦 ∈ {𝑧 ∣ ∃𝑥 ∈ 𝐴 𝑧 = 𝐵}𝑦)

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  ∀wral 3064  ∃wrex 3065  Vcvv 3432  ⦋csb 3832  {csn 4561  ∪ cuni 4839  Disj wdisj 5039

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-nf 1787  df-sb 2068  df-mo 2540  df-clab 2716  df-cleq 2730  df-clel 2816  df-nfc 2889  df-ne 2944  df-ral 3069  df-rex 3070  df-rmo 3071  df-rab 3073  df-v 3434  df-sbc 3717  df-csb 3833  df-dif 3890  df-un 3892  df-in 3894  df-ss 3904  df-nul 4257  df-sn 4562  df-pr 4564  df-uni 4840  df-disj 5040

This theorem is referenced by:  disjrnmpt  30924