Metamath Proof Explorer

Theorem disjressuc2

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

Ref Expression
Assertion disjressuc2 ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u R ∩ A R = ∅

Proof

Step Hyp Ref Expression
1 eqeq1 ⊢ u = A → u = v ↔ A = v
2 eceq1 ⊢ u = A → u R = A R
3 2 ineq1d ⊢ u = A → u R ∩ v R = A R ∩ v R
4 3 eqeq1d ⊢ u = A → u R ∩ v R = ∅ ↔ A R ∩ v R = ∅
5 1 4 orbi12d ⊢ u = A → u = v ∨ u R ∩ v R = ∅ ↔ A = v ∨ A R ∩ v R = ∅
6 eqeq2 ⊢ v = A → u = v ↔ u = A
7 eceq1 ⊢ v = A → v R = A R
8 7 ineq2d ⊢ v = A → u R ∩ v R = u R ∩ A R
9 8 eqeq1d ⊢ v = A → u R ∩ v R = ∅ ↔ u R ∩ A R = ∅
10 6 9 orbi12d ⊢ v = A → u = v ∨ u R ∩ v R = ∅ ↔ u = A ∨ u R ∩ A R = ∅
11 eqeq1 ⊢ u = A → u = A ↔ A = A
12 2 ineq1d ⊢ u = A → u R ∩ A R = A R ∩ A R
13 12 eqeq1d ⊢ u = A → u R ∩ A R = ∅ ↔ A R ∩ A R = ∅
14 11 13 orbi12d ⊢ u = A → u = A ∨ u R ∩ A R = ∅ ↔ A = A ∨ A R ∩ A R = ∅
15 5 10 14 2ralunsn ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ∧ A = A ∨ A R ∩ A R = ∅
16 eqid ⊢ A = A
17 16 orci ⊢ A = A ∨ A R ∩ A R = ∅
18 17 biantru ⊢ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ↔ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ∧ A = A ∨ A R ∩ A R = ∅
19 18 anbi2i ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ∧ A = A ∨ A R ∩ A R = ∅
20 15 19 bitr4di ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
21 eqeq1 ⊢ u = v → u = A ↔ v = A
22 eqcom ⊢ v = A ↔ A = v
23 21 22 bitrdi ⊢ u = v → u = A ↔ A = v
24 eceq1 ⊢ u = v → u R = v R
25 24 ineq1d ⊢ u = v → u R ∩ A R = v R ∩ A R
26 incom ⊢ v R ∩ A R = A R ∩ v R
27 25 26 eqtrdi ⊢ u = v → u R ∩ A R = A R ∩ v R
28 27 eqeq1d ⊢ u = v → u R ∩ A R = ∅ ↔ A R ∩ v R = ∅
29 23 28 orbi12d ⊢ u = v → u = A ∨ u R ∩ A R = ∅ ↔ A = v ∨ A R ∩ v R = ∅
30 29 cbvralvw ⊢ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ↔ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
31 30 biimpi ⊢ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ → ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
32 31 pm4.71i ⊢ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ↔ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
33 32 anbi2i ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
34 3anass ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
35 df-3an ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅
36 33 34 35 3bitr2ri ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅ ∧ ∀ v ∈ A A = v ∨ A R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅
37 20 36 bitrdi ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅
38 elneq ⊢ u ∈ A → u ≠ A
39 38 neneqd ⊢ u ∈ A → ¬ u = A
40 39 biorfd ⊢ u ∈ A → u R ∩ A R = ∅ ↔ u = A ∨ u R ∩ A R = ∅
41 40 ralbiia ⊢ ∀ u ∈ A u R ∩ A R = ∅ ↔ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅
42 41 anbi2i ⊢ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u R ∩ A R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u = A ∨ u R ∩ A R = ∅
43 37 42 bitr4di ⊢ A ∈ V → ∀ u ∈ A ∪ A ∀ v ∈ A ∪ A u = v ∨ u R ∩ v R = ∅ ↔ ∀ u ∈ A ∀ v ∈ A u = v ∨ u R ∩ v R = ∅ ∧ ∀ u ∈ A u R ∩ A R = ∅