Theorem idjudju 17252

Description: An indexed disjoint union over two sets equals the disjoint union of those two sets. This connects our notation for an indexed disjoint union, ∪ 𝑥 ∈ 𝐶({𝑥} × 𝐹) which uses df-iun 4014, with our notation for the disjoint union of two sets (df-dju 7384). (Contributed by Jim Kingdon, 2-Oct-2026.)

Hypothesis

Ref	Expression
idjudju.f	⊢ 𝐹 = if(𝑥 = ∅, 𝐴, 𝐵)

Assertion

Ref	Expression
idjudju	⊢ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) = (𝐴 ⊔ 𝐵)

Distinct variable groups:   𝑥,𝐴   𝑥,𝐵

Allowed substitution hint:   𝐹(𝑥)

Proof of Theorem idjudju

Dummy variables 𝑦 𝑧 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		eliunxp 4921	. . . 4 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) ↔ ∃𝑥∃𝑧(𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)))
2		simpl 109	. . . . . 6 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)) → 𝑦 = ⟨𝑥, 𝑧⟩)
3		anass 405	. . . . . . . 8 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 ∈ 2o) ↔ (𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑧 ∈ 𝐹 ∧ 𝑥 ∈ 2o)))
4		ancom 266	. . . . . . . . 9 ⊢ ((𝑧 ∈ 𝐹 ∧ 𝑥 ∈ 2o) ↔ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹))
5	4	anbi2i 461	. . . . . . . 8 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑧 ∈ 𝐹 ∧ 𝑥 ∈ 2o)) ↔ (𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)))
6	3, 5	bitri 184	. . . . . . 7 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 ∈ 2o) ↔ (𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)))
7		elpri 3732	. . . . . . . . 9 ⊢ (𝑥 ∈ {∅, 1o} → (𝑥 = ∅ ∨ 𝑥 = 1o))
8		df2o3 6706	. . . . . . . . 9 ⊢ 2o = {∅, 1o}
9	7, 8	eleq2s 2333	. . . . . . . 8 ⊢ (𝑥 ∈ 2o → (𝑥 = ∅ ∨ 𝑥 = 1o))
10		ssun1 3392	. . . . . . . . . . 11 ⊢ ({∅} × 𝐴) ⊆ (({∅} × 𝐴) ∪ ({1o} × 𝐵))
11		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → 𝑥 = ∅)
12		0ex 4262	. . . . . . . . . . . . . 14 ⊢ ∅ ∈ V
13	12	snid 3740	. . . . . . . . . . . . 13 ⊢ ∅ ∈ {∅}
14	11, 13	eqeltrdi 2329	. . . . . . . . . . . 12 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → 𝑥 ∈ {∅})
15	11	notnotd 639	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ¬ ¬ 𝑥 = ∅)
16	15	intnanrd 944	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ¬ (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵))
17		idjudju.f	. . . . . . . . . . . . . . . . . 18 ⊢ 𝐹 = if(𝑥 = ∅, 𝐴, 𝐵)
18	17	eleq2i 2305	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ 𝐹 ↔ 𝑧 ∈ if(𝑥 = ∅, 𝐴, 𝐵))
19		elif 3652	. . . . . . . . . . . . . . . . 17 ⊢ (𝑧 ∈ if(𝑥 = ∅, 𝐴, 𝐵) ↔ ((𝑥 = ∅ ∧ 𝑧 ∈ 𝐴) ∨ (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵)))
20	18, 19	bitri 184	. . . . . . . . . . . . . . . 16 ⊢ (𝑧 ∈ 𝐹 ↔ ((𝑥 = ∅ ∧ 𝑧 ∈ 𝐴) ∨ (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵)))
21	20	bilani 387	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) → ((𝑥 = ∅ ∧ 𝑧 ∈ 𝐴) ∨ (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵)))
22	21	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ((𝑥 = ∅ ∧ 𝑧 ∈ 𝐴) ∨ (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵)))
23	16, 22	ecased 1390	. . . . . . . . . . . . 13 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → (𝑥 = ∅ ∧ 𝑧 ∈ 𝐴))
24	23	simprd 114	. . . . . . . . . . . 12 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → 𝑧 ∈ 𝐴)
25	14, 24	opelxpd 4809	. . . . . . . . . . 11 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ⟨𝑥, 𝑧⟩ ∈ ({∅} × 𝐴))
26	10, 25	sselid 3246	. . . . . . . . . 10 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ⟨𝑥, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
27		df-dju 7384	. . . . . . . . . 10 ⊢ (𝐴 ⊔ 𝐵) = (({∅} × 𝐴) ∪ ({1o} × 𝐵))
28	26, 27	eleqtrrdi 2332	. . . . . . . . 9 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = ∅) → ⟨𝑥, 𝑧⟩ ∈ (𝐴 ⊔ 𝐵))
29		ssun2 3393	. . . . . . . . . . 11 ⊢ ({1o} × 𝐵) ⊆ (({∅} × 𝐴) ∪ ({1o} × 𝐵))
30		simpr 110	. . . . . . . . . . . . 13 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → 𝑥 = 1o)
31		1oex 6699	. . . . . . . . . . . . . 14 ⊢ 1o ∈ V
32	31	snid 3740	. . . . . . . . . . . . 13 ⊢ 1o ∈ {1o}
33	30, 32	eqeltrdi 2329	. . . . . . . . . . . 12 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → 𝑥 ∈ {1o})
34		1n0 6709	. . . . . . . . . . . . . . . . . 18 ⊢ 1o ≠ ∅
35	34	neii 2422	. . . . . . . . . . . . . . . . 17 ⊢ ¬ 1o = ∅
36		eqtr2 2257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑥 = 1o ∧ 𝑥 = ∅) → 1o = ∅)
37	36	ex 115	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 = 1o → (𝑥 = ∅ → 1o = ∅))
38	35, 37	mtoi 674	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 = 1o → ¬ 𝑥 = ∅)
39	38	adantl 277	. . . . . . . . . . . . . . 15 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ¬ 𝑥 = ∅)
40	39	intnanrd 944	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ¬ (𝑥 = ∅ ∧ 𝑧 ∈ 𝐴))
41	21	orcomd 741	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) → ((¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵) ∨ (𝑥 = ∅ ∧ 𝑧 ∈ 𝐴)))
42	41	adantr 276	. . . . . . . . . . . . . 14 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ((¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵) ∨ (𝑥 = ∅ ∧ 𝑧 ∈ 𝐴)))
43	40, 42	ecased 1390	. . . . . . . . . . . . 13 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → (¬ 𝑥 = ∅ ∧ 𝑧 ∈ 𝐵))
44	43	simprd 114	. . . . . . . . . . . 12 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → 𝑧 ∈ 𝐵)
45	33, 44	opelxpd 4809	. . . . . . . . . . 11 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ⟨𝑥, 𝑧⟩ ∈ ({1o} × 𝐵))
46	29, 45	sselid 3246	. . . . . . . . . 10 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ⟨𝑥, 𝑧⟩ ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
47	46, 27	eleqtrrdi 2332	. . . . . . . . 9 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 = 1o) → ⟨𝑥, 𝑧⟩ ∈ (𝐴 ⊔ 𝐵))
48	28, 47	jaodan 809	. . . . . . . 8 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ (𝑥 = ∅ ∨ 𝑥 = 1o)) → ⟨𝑥, 𝑧⟩ ∈ (𝐴 ⊔ 𝐵))
49	9, 48	sylan2 286	. . . . . . 7 ⊢ (((𝑦 = ⟨𝑥, 𝑧⟩ ∧ 𝑧 ∈ 𝐹) ∧ 𝑥 ∈ 2o) → ⟨𝑥, 𝑧⟩ ∈ (𝐴 ⊔ 𝐵))
50	6, 49	sylbir 135	. . . . . 6 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)) → ⟨𝑥, 𝑧⟩ ∈ (𝐴 ⊔ 𝐵))
51	2, 50	eqeltrd 2315	. . . . 5 ⊢ ((𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)) → 𝑦 ∈ (𝐴 ⊔ 𝐵))
52	51	exlimivv 1952	. . . 4 ⊢ (∃𝑥∃𝑧(𝑦 = ⟨𝑥, 𝑧⟩ ∧ (𝑥 ∈ 2o ∧ 𝑧 ∈ 𝐹)) → 𝑦 ∈ (𝐴 ⊔ 𝐵))
53	1, 52	sylbi 121	. . 3 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) → 𝑦 ∈ (𝐴 ⊔ 𝐵))
54	27	eleq2i 2305	. . . . 5 ⊢ (𝑦 ∈ (𝐴 ⊔ 𝐵) ↔ 𝑦 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)))
55		elun 3370	. . . . 5 ⊢ (𝑦 ∈ (({∅} × 𝐴) ∪ ({1o} × 𝐵)) ↔ (𝑦 ∈ ({∅} × 𝐴) ∨ 𝑦 ∈ ({1o} × 𝐵)))
56	54, 55	bitri 184	. . . 4 ⊢ (𝑦 ∈ (𝐴 ⊔ 𝐵) ↔ (𝑦 ∈ ({∅} × 𝐴) ∨ 𝑦 ∈ ({1o} × 𝐵)))
57		1st2nd2 6413	. . . . . 6 ⊢ (𝑦 ∈ ({∅} × 𝐴) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
58		xp1st 6403	. . . . . . . . 9 ⊢ (𝑦 ∈ ({∅} × 𝐴) → (1st ‘𝑦) ∈ {∅})
59		elsni 3727	. . . . . . . . 9 ⊢ ((1st ‘𝑦) ∈ {∅} → (1st ‘𝑦) = ∅)
60	58, 59	syl 14	. . . . . . . 8 ⊢ (𝑦 ∈ ({∅} × 𝐴) → (1st ‘𝑦) = ∅)
61		0lt2o 6718	. . . . . . . 8 ⊢ ∅ ∈ 2o
62	60, 61	eqeltrdi 2329	. . . . . . 7 ⊢ (𝑦 ∈ ({∅} × 𝐴) → (1st ‘𝑦) ∈ 2o)
63		xp2nd 6404	. . . . . . . 8 ⊢ (𝑦 ∈ ({∅} × 𝐴) → (2nd ‘𝑦) ∈ 𝐴)
64	60	iftrued 3647	. . . . . . . 8 ⊢ (𝑦 ∈ ({∅} × 𝐴) → if((1st ‘𝑦) = ∅, 𝐴, 𝐵) = 𝐴)
65	63, 64	eleqtrrd 2318	. . . . . . 7 ⊢ (𝑦 ∈ ({∅} × 𝐴) → (2nd ‘𝑦) ∈ if((1st ‘𝑦) = ∅, 𝐴, 𝐵))
66		eqeq1 2245	. . . . . . . . . 10 ⊢ (𝑥 = (1st ‘𝑦) → (𝑥 = ∅ ↔ (1st ‘𝑦) = ∅))
67	66	ifbid 3662	. . . . . . . . 9 ⊢ (𝑥 = (1st ‘𝑦) → if(𝑥 = ∅, 𝐴, 𝐵) = if((1st ‘𝑦) = ∅, 𝐴, 𝐵))
68	17, 67	eqtrid 2283	. . . . . . . 8 ⊢ (𝑥 = (1st ‘𝑦) → 𝐹 = if((1st ‘𝑦) = ∅, 𝐴, 𝐵))
69	68	opeliunxp2 4922	. . . . . . 7 ⊢ (⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) ↔ ((1st ‘𝑦) ∈ 2o ∧ (2nd ‘𝑦) ∈ if((1st ‘𝑦) = ∅, 𝐴, 𝐵)))
70	62, 65, 69	sylanbrc 421	. . . . . 6 ⊢ (𝑦 ∈ ({∅} × 𝐴) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
71	57, 70	eqeltrd 2315	. . . . 5 ⊢ (𝑦 ∈ ({∅} × 𝐴) → 𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
72		1st2nd2 6413	. . . . . 6 ⊢ (𝑦 ∈ ({1o} × 𝐵) → 𝑦 = ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩)
73		xp1st 6403	. . . . . . . . 9 ⊢ (𝑦 ∈ ({1o} × 𝐵) → (1st ‘𝑦) ∈ {1o})
74		elsni 3727	. . . . . . . . 9 ⊢ ((1st ‘𝑦) ∈ {1o} → (1st ‘𝑦) = 1o)
75	73, 74	syl 14	. . . . . . . 8 ⊢ (𝑦 ∈ ({1o} × 𝐵) → (1st ‘𝑦) = 1o)
76		1lt2o 6719	. . . . . . . 8 ⊢ 1o ∈ 2o
77	75, 76	eqeltrdi 2329	. . . . . . 7 ⊢ (𝑦 ∈ ({1o} × 𝐵) → (1st ‘𝑦) ∈ 2o)
78		xp2nd 6404	. . . . . . . 8 ⊢ (𝑦 ∈ ({1o} × 𝐵) → (2nd ‘𝑦) ∈ 𝐵)
79		eqtr2 2257	. . . . . . . . . . . 12 ⊢ (((1st ‘𝑦) = 1o ∧ (1st ‘𝑦) = ∅) → 1o = ∅)
80	79	ex 115	. . . . . . . . . . 11 ⊢ ((1st ‘𝑦) = 1o → ((1st ‘𝑦) = ∅ → 1o = ∅))
81	35, 80	mtoi 674	. . . . . . . . . 10 ⊢ ((1st ‘𝑦) = 1o → ¬ (1st ‘𝑦) = ∅)
82	75, 81	syl 14	. . . . . . . . 9 ⊢ (𝑦 ∈ ({1o} × 𝐵) → ¬ (1st ‘𝑦) = ∅)
83	82	iffalsed 3650	. . . . . . . 8 ⊢ (𝑦 ∈ ({1o} × 𝐵) → if((1st ‘𝑦) = ∅, 𝐴, 𝐵) = 𝐵)
84	78, 83	eleqtrrd 2318	. . . . . . 7 ⊢ (𝑦 ∈ ({1o} × 𝐵) → (2nd ‘𝑦) ∈ if((1st ‘𝑦) = ∅, 𝐴, 𝐵))
85	77, 84, 69	sylanbrc 421	. . . . . 6 ⊢ (𝑦 ∈ ({1o} × 𝐵) → ⟨(1st ‘𝑦), (2nd ‘𝑦)⟩ ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
86	72, 85	eqeltrd 2315	. . . . 5 ⊢ (𝑦 ∈ ({1o} × 𝐵) → 𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
87	71, 86	jaoi 728	. . . 4 ⊢ ((𝑦 ∈ ({∅} × 𝐴) ∨ 𝑦 ∈ ({1o} × 𝐵)) → 𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
88	56, 87	sylbi 121	. . 3 ⊢ (𝑦 ∈ (𝐴 ⊔ 𝐵) → 𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹))
89	53, 88	impbii 126	. 2 ⊢ (𝑦 ∈ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) ↔ 𝑦 ∈ (𝐴 ⊔ 𝐵))
90	89	eqriv 2235	1 ⊢ ∪ 𝑥 ∈ 2o ({𝑥} × 𝐹) = (𝐴 ⊔ 𝐵)

This proof depends on syntax axioms:  ¬ wn 3   ∧ wa 104   ∨ wo 720   = wceq 1402  ∃wex 1545   ∈ wcel 2209   ∪ cun 3218  ∅c0 3520  ifcif 3638  {csn 3709  {cpr 3710  ⟨cop 3712  ∪ ciun 4012   × cxp 4774  ‘cfv 5380  1^st c1st 6376  2^nd c2nd 6377  1_oc1o 6684  2_oc2o 6685   ⊔ cdju 7383

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-in1 623  ax-in2 624  ax-io 721  ax-5 1500  ax-7 1501  ax-gen 1502  ax-ie1 1546  ax-ie2 1547  ax-8 1557  ax-10 1558  ax-11 1559  ax-i12 1560  ax-bndl 1562  ax-4 1563  ax-17 1579  ax-i9 1583  ax-ial 1587  ax-i5r 1588  ax-14 2212  ax-ext 2220  ax-sep 4251  ax-nul 4261  ax-pow 4313  ax-pr 4348  ax-un 4580

This proof depends on definitions:  df-bi 117  df-3an 1011  df-tru 1405  df-nf 1514  df-sb 1816  df-eu 2089  df-mo 2090  df-clab 2225  df-cleq 2231  df-clel 2234  df-nfc 2381  df-ne 2421  df-ral 2533  df-rex 2534  df-v 2823  df-sbc 3052  df-csb 3148  df-dif 3222  df-un 3224  df-in 3226  df-ss 3233  df-nul 3521  df-if 3639  df-pw 3690  df-sn 3715  df-pr 3716  df-op 3718  df-uni 3936  df-iun 4014  df-br 4132  df-opab 4194  df-mpt 4195  df-tr 4232  df-id 4440  df-iord 4513  df-on 4515  df-suc 4518  df-xp 4782  df-rel 4783  df-cnv 4784  df-co 4785  df-dm 4786  df-rn 4787  df-iota 5340  df-fun 5382  df-fv 5388  df-1st 6378  df-2nd 6379  df-1o 6691  df-2o 6692  df-dju 7384

This theorem is used by: (None)