Theorem disjressuc2 37561

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 2734	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝑣 ↔ 𝐴 = 𝑣))
2		eceq1 8743	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → [𝑢]𝑅 = [𝐴]𝑅)
3	2	ineq1d 4210	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
4	3	eqeq1d 2732	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
5	1, 4	orbi12d 915	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
6		eqeq2 2742	. . . . . 6 ⊢ (𝑣 = 𝐴 → (𝑢 = 𝑣 ↔ 𝑢 = 𝐴))
7		eceq1 8743	. . . . . . . 8 ⊢ (𝑣 = 𝐴 → [𝑣]𝑅 = [𝐴]𝑅)
8	7	ineq2d 4211	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝑢]𝑅 ∩ [𝐴]𝑅))
9	8	eqeq1d 2732	. . . . . 6 ⊢ (𝑣 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
10	6, 9	orbi12d 915	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
11		eqeq1 2734	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝐴 ↔ 𝐴 = 𝐴))
12	2	ineq1d 4210	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝐴]𝑅))
13	12	eqeq1d 2732	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))
14	11, 13	orbi12d 915	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
15	5, 10, 14	2ralunsn 4894	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))))
16		eqid 2730	. . . . . . 7 ⊢ 𝐴 = 𝐴
17	16	orci 861	. . . . . 6 ⊢ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)
18	17	biantru 528	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
19	18	anbi2i 621	. . . 4 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))))
20	15, 19	bitr4di 288	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
21		eqeq1 2734	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝑣 = 𝐴))
22		eqcom 2737	. . . . . . . . . 10 ⊢ (𝑣 = 𝐴 ↔ 𝐴 = 𝑣)
23	21, 22	bitrdi 286	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝐴 = 𝑣))
24		eceq1 8743	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → [𝑢]𝑅 = [𝑣]𝑅)
25	24	ineq1d 4210	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝑣]𝑅 ∩ [𝐴]𝑅))
26		incom 4200	. . . . . . . . . . 11 ⊢ ([𝑣]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅)
27	25, 26	eqtrdi 2786	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
28	27	eqeq1d 2732	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
29	23, 28	orbi12d 915	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
30	29	cbvralvw 3232	. . . . . . 7 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
31	30	biimpi 215	. . . . . 6 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) → ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
32	31	pm4.71i 558	. . . . 5 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
33	32	anbi2i 621	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
34		3anass 1093	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
35		df-3an 1087	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
36	33, 34, 35	3bitr2ri 299	. . 3 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
37	20, 36	bitrdi 286	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
38		elneq 9595	. . . . . 6 ⊢ (𝑢 ∈ 𝐴 → 𝑢 ≠ 𝐴)
39	38	neneqd 2943	. . . . 5 ⊢ (𝑢 ∈ 𝐴 → ¬ 𝑢 = 𝐴)
40	39	biorfd 37400	. . . 4 ⊢ (𝑢 ∈ 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
41	40	ralbiia 3089	. . 3 ⊢ (∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
42	41	anbi2i 621	. 2 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
43	37, 42	bitr4di 288	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 394   ∨ wo 843   ∧ w3a 1085   = wceq 1539   ∈ wcel 2104  ∀wral 3059   ∪ cun 3945   ∩ cin 3946  ∅c0 4321  {csn 4627  [cec 8703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-10 2135  ax-12 2169  ax-ext 2701  ax-sep 5298  ax-pr 5426  ax-reg 9589

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-ne 2939  df-ral 3060  df-rex 3069  df-rab 3431  df-v 3474  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688  df-ec 8707

This theorem is referenced by:  disjsuc2  37564