Theorem disjabrexf 30922

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

Hypothesis

Ref	Expression
disjabrexf.1	⊢ Ⅎ𝑥𝐴

Assertion

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

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

Allowed substitution hints:   𝐴(𝑥)   𝐵(𝑥)

Proof of Theorem disjabrexf

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

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 396   = wceq 1539   ∈ wcel 2106  {cab 2715  Ⅎwnfc 2887  ∀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:  measvunilem  32180