Theorem disjressuc2 38785

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 2744	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝑣 ↔ 𝐴 = 𝑣))
2		eceq1 8680	. . . . . . . 8 ⊢ (𝑢 = 𝐴 → [𝑢]𝑅 = [𝐴]𝑅)
3	2	ineq1d 4155	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
4	3	eqeq1d 2742	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
5	1, 4	orbi12d 924	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
6		eqeq2 2752	. . . . . 6 ⊢ (𝑣 = 𝐴 → (𝑢 = 𝑣 ↔ 𝑢 = 𝐴))
7		eceq1 8680	. . . . . . . 8 ⊢ (𝑣 = 𝐴 → [𝑣]𝑅 = [𝐴]𝑅)
8	7	ineq2d 4156	. . . . . . 7 ⊢ (𝑣 = 𝐴 → ([𝑢]𝑅 ∩ [𝑣]𝑅) = ([𝑢]𝑅 ∩ [𝐴]𝑅))
9	8	eqeq1d 2742	. . . . . 6 ⊢ (𝑣 = 𝐴 → (([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅ ↔ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
10	6, 9	orbi12d 924	. . . . 5 ⊢ (𝑣 = 𝐴 → ((𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
11		eqeq1 2744	. . . . . 6 ⊢ (𝑢 = 𝐴 → (𝑢 = 𝐴 ↔ 𝐴 = 𝐴))
12	2	ineq1d 4155	. . . . . . 7 ⊢ (𝑢 = 𝐴 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝐴]𝑅))
13	12	eqeq1d 2742	. . . . . 6 ⊢ (𝑢 = 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))
14	11, 13	orbi12d 924	. . . . 5 ⊢ (𝑢 = 𝐴 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
15	5, 10, 14	2ralunsn 4833	. . . 4 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))))
16		eqid 2740	. . . . . . 7 ⊢ 𝐴 = 𝐴
17	16	orci 871	. . . . . 6 ⊢ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)
18	17	biantru 534	. . . . 5 ⊢ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅)))
19	18	anbi2i 629	. . . 4 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ (∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (𝐴 = 𝐴 ∨ ([𝐴]𝑅 ∩ [𝐴]𝑅) = ∅))))
20	15, 19	bitr4di 290	. . 3 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
21		eqeq1 2744	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝑣 = 𝐴))
22		eqcom 2747	. . . . . . . . . 10 ⊢ (𝑣 = 𝐴 ↔ 𝐴 = 𝑣)
23	21, 22	bitrdi 288	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (𝑢 = 𝐴 ↔ 𝐴 = 𝑣))
24		eceq1 8680	. . . . . . . . . . . 12 ⊢ (𝑢 = 𝑣 → [𝑢]𝑅 = [𝑣]𝑅)
25	24	ineq1d 4155	. . . . . . . . . . 11 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝑣]𝑅 ∩ [𝐴]𝑅))
26		incom 4145	. . . . . . . . . . 11 ⊢ ([𝑣]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅)
27	25, 26	eqtrdi 2791	. . . . . . . . . 10 ⊢ (𝑢 = 𝑣 → ([𝑢]𝑅 ∩ [𝐴]𝑅) = ([𝐴]𝑅 ∩ [𝑣]𝑅))
28	27	eqeq1d 2742	. . . . . . . . 9 ⊢ (𝑢 = 𝑣 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
29	23, 28	orbi12d 924	. . . . . . . 8 ⊢ (𝑢 = 𝑣 → ((𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
30	29	cbvralvw 3218	. . . . . . 7 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
31	30	biimpi 217	. . . . . 6 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) → ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))
32	31	pm4.71i 564	. . . . 5 ⊢ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
33	32	anbi2i 629	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
34		3anass 1100	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ (∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅))))
35		df-3an 1094	. . . 4 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)))
36	33, 34, 35	3bitr2ri 301	. . 3 ⊢ (((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)) ∧ ∀𝑣 ∈ 𝐴 (𝐴 = 𝑣 ∨ ([𝐴]𝑅 ∩ [𝑣]𝑅) = ∅)) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
37	20, 36	bitrdi 288	. 2 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))))
38		elneq 9513	. . . . . 6 ⊢ (𝑢 ∈ 𝐴 → 𝑢 ≠ 𝐴)
39	38	neneqd 2940	. . . . 5 ⊢ (𝑢 ∈ 𝐴 → ¬ 𝑢 = 𝐴)
40	39	biorfd 38611	. . . 4 ⊢ (𝑢 ∈ 𝐴 → (([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
41	40	ralbiia 3084	. . 3 ⊢ (∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅ ↔ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅))
42	41	anbi2i 629	. 2 ⊢ ((∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 (𝑢 = 𝐴 ∨ ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))
43	37, 42	bitr4di 290	1 ⊢ (𝐴 ∈ 𝑉 → (∀𝑢 ∈ (𝐴 ∪ {𝐴})∀𝑣 ∈ (𝐴 ∪ {𝐴})(𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ↔ (∀𝑢 ∈ 𝐴 ∀𝑣 ∈ 𝐴 (𝑢 = 𝑣 ∨ ([𝑢]𝑅 ∩ [𝑣]𝑅) = ∅) ∧ ∀𝑢 ∈ 𝐴 ([𝑢]𝑅 ∩ [𝐴]𝑅) = ∅)))

Syntax hints:   → wi 4   ↔ wb 207   ∧ wa 396   ∨ wo 853   ∧ w3a 1092   = wceq 1547   ∈ wcel 2119  ∀wral 3054   ∪ cun 3888   ∩ cin 3889  ∅c0 4268  {csn 4562  [cec 8638

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-reg 9504

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-ne 2936  df-ral 3055  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638  df-ec 8642

This theorem is referenced by:  disjsuc2  38788