Theorem disjressuc2 37247

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 2737	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝑣 ↔ 𝐴 = 𝑣))
2		eceq1 8738	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → [𝑢]𝑅 = [𝐴]𝑅)
3	2	ineq1d 4211	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
4	3	eqeq1d 2735	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
5	1, 4	orbi12d 918	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
6		eqeq2 2745	. . . . . 6 ⊢ (𝑣 = 𝐴 → (𝑢 = 𝑣 ↔ 𝑢 = 𝐴))
7		eceq1 8738	. . . . . . . 8 ⊢ (𝑣 = 𝐴 → [𝑣]𝑅 = [𝐴]𝑅)
8	7	ineq2d 4212	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝑢]𝑅 ∩ [𝐴]𝑅))
9	8	eqeq1d 2735	. . . . . 6 ⊢ (𝑣 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
10	6, 9	orbi12d 918	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
11		eqeq1 2737	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝐴 ↔ 𝐴 = 𝐴))
12	2	ineq1d 4211	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝐴]𝑅))
13	12	eqeq1d 2735	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))
14	11, 13	orbi12d 918	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
15	5, 10, 14	2ralunsn 4895	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))))
16		eqid 2733	. . . . . . 7 ⊢ 𝐴 = 𝐴
17	16	orci 864	. . . . . 6 ⊢ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)
18	17	biantru 531	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
19	18	anbi2i 624	. . . 4 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))))
20	15, 19	bitr4di 289	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
21		eqeq1 2737	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝑣 = 𝐴))
22		eqcom 2740	. . . . . . . . . 10 ⊢ (𝑣 = 𝐴 ↔ 𝐴 = 𝑣)
23	21, 22	bitrdi 287	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝐴 = 𝑣))
24		eceq1 8738	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → [𝑢]𝑅 = [𝑣]𝑅)
25	24	ineq1d 4211	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝑣]𝑅 ∩ [𝐴]𝑅))
26		incom 4201	. . . . . . . . . . 11 ⊢ ([𝑣]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅)
27	25, 26	eqtrdi 2789	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
28	27	eqeq1d 2735	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
29	23, 28	orbi12d 918	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
30	29	cbvralvw 3235	. . . . . . 7 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
31	30	biimpi 215	. . . . . 6 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) → ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
32	31	pm4.71i 561	. . . . 5 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
33	32	anbi2i 624	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
34		3anass 1096	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
35		df-3an 1090	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
36	33, 34, 35	3bitr2ri 300	. . 3 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
37	20, 36	bitrdi 287	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
38		elneq 9590	. . . . . 6 ⊢ (𝑢 ∈ 𝐴 → 𝑢 ≠ 𝐴)
39	38	neneqd 2946	. . . . 5 ⊢ (𝑢 ∈ 𝐴 → ¬ 𝑢 = 𝐴)
40	39	biorfd 37086	. . . 4 ⊢ (𝑢 ∈ 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
41	40	ralbiia 3092	. . 3 ⊢ (∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
42	41	anbi2i 624	. 2 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
43	37, 42	bitr4di 289	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))

Syntax hints:   → wi 4   ↔ wb 205   ∧ wa 397   ∨ wo 846   ∧ w3a 1088   = wceq 1542   ∈ wcel 2107  ∀wral 3062   ∪ cun 3946   ∩ cin 3947  ∅c0 4322  {csn 4628  [cec 8698

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 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-12 2172  ax-ext 2704  ax-sep 5299  ax-pr 5427  ax-reg 9584

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-ne 2942  df-ral 3063  df-rex 3072  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-xp 5682  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689  df-ec 8702

This theorem is referenced by:  disjsuc2  37250