Theorem disjressuc2 38596

Description: Double restricted quantification over the union of a set and its singleton. (Contributed by Peter Mazsa, 22-Aug-2023.)

Assertion

Ref	Expression
disjressuc2	⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))

Distinct variable groups:   𝑢,𝐴,𝑣   𝑢,𝑅,𝑣   𝑢,𝑉

Allowed substitution hint:   𝑉(𝑣)

Proof of Theorem disjressuc2

Step	Hyp	Ref	Expression
1		eqeq1 2740	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝑣 ↔ 𝐴 = 𝑣))
2		eceq1 8674	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → [𝑢]𝑅 = [𝐴]𝑅)
3	2	ineq1d 4171	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
4	3	eqeq1d 2738	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
5	1, 4	orbi12d 918	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
6		eqeq2 2748	. . . . . 6 ⊢ (𝑣 = 𝐴 → (𝑢 = 𝑣 ↔ 𝑢 = 𝐴))
7		eceq1 8674	. . . . . . . 8 ⊢ (𝑣 = 𝐴 → [𝑣]𝑅 = [𝐴]𝑅)
8	7	ineq2d 4172	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝑢]𝑅 ∩ [𝐴]𝑅))
9	8	eqeq1d 2738	. . . . . 6 ⊢ (𝑣 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
10	6, 9	orbi12d 918	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
11		eqeq1 2740	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝐴 ↔ 𝐴 = 𝐴))
12	2	ineq1d 4171	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝐴]𝑅))
13	12	eqeq1d 2738	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))
14	11, 13	orbi12d 918	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
15	5, 10, 14	2ralunsn 4851	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))))
16		eqid 2736	. . . . . . 7 ⊢ 𝐴 = 𝐴
17	16	orci 865	. . . . . 6 ⊢ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)
18	17	biantru 529	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
19	18	anbi2i 623	. . . 4 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))))
20	15, 19	bitr4di 289	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
21		eqeq1 2740	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝑣 = 𝐴))
22		eqcom 2743	. . . . . . . . . 10 ⊢ (𝑣 = 𝐴 ↔ 𝐴 = 𝑣)
23	21, 22	bitrdi 287	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝐴 = 𝑣))
24		eceq1 8674	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → [𝑢]𝑅 = [𝑣]𝑅)
25	24	ineq1d 4171	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝑣]𝑅 ∩ [𝐴]𝑅))
26		incom 4161	. . . . . . . . . . 11 ⊢ ([𝑣]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅)
27	25, 26	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
28	27	eqeq1d 2738	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
29	23, 28	orbi12d 918	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
30	29	cbvralvw 3214	. . . . . . 7 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
31	30	biimpi 216	. . . . . 6 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) → ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
32	31	pm4.71i 559	. . . . 5 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
33	32	anbi2i 623	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
34		3anass 1094	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
35		df-3an 1088	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
36	33, 34, 35	3bitr2ri 300	. . 3 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
37	20, 36	bitrdi 287	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
38		elneq 9505	. . . . . 6 ⊢ (𝑢 ∈ 𝐴 → 𝑢 ≠ 𝐴)
39	38	neneqd 2937	. . . . 5 ⊢ (𝑢 ∈ 𝐴 → ¬ 𝑢 = 𝐴)
40	39	biorfd 38433	. . . 4 ⊢ (𝑢 ∈ 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
41	40	ralbiia 3080	. . 3 ⊢ (∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
42	41	anbi2i 623	. 2 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
43	37, 42	bitr4di 289	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))

Syntax hints:   → wi 4   ↔ wb 206   ∧ wa 395   ∨ wo 847   ∧ w3a 1086   = wceq 1541   ∈ wcel 2113  ∀wral 3051   ∪ cun 3899   ∩ cin 3900  ∅c0 4285  {csn 4580  [cec 8633

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-pr 5377  ax-reg 9497

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-ne 2933  df-ral 3052  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637  df-ec 8637

This theorem is referenced by:  disjsuc2  38599