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 ( 𝐴 ∈ 𝑉 → ( ∀ 𝑢 ∈ ( 𝐴 ∪ { 𝐴 } ) ∀ 𝑣 ∈ ( 𝐴 ∪ { 𝐴 } ) ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ↔ ( ∀ 𝑢 ∈ 𝐴 ∀ 𝑣 ∈ 𝐴 ( 𝑢 = 𝑣 ∨ ( [ 𝑢 ] 𝑅 ∩ [ 𝑣 ] 𝑅 ) = ∅ ) ∧ ∀ 𝑢 ∈ 𝐴 ( [ 𝑢 ] 𝑅 ∩ [ 𝐴 ] 𝑅 ) = ∅ ) ) )

Proof

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