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∪Au=v∨uR∩vR=∅↔∀u∈A∀v∈Au=v∨uR∩vR=∅∧∀u∈AuR∩AR=∅

Proof

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