Metamath Proof Explorer

Theorem clwwlknondisj

Description: The sets of closed walks on different vertices are disjunct. (Contributed by Alexander van der Vekens, 7-Oct-2018) (Revised by AV, 28-May-2021) (Revised by AV, 3-Mar-2022) (Proof shortened by AV, 28-Mar-2022)

Ref Expression
Assertion clwwlknondisj ⊢ Disj x ∈ V x ClWWalksNOn ⁡ G N

Proof

Step Hyp Ref Expression
1 clwwlknon ⊢ x ClWWalksNOn ⁡ G N = w ∈ N ClWWalksN G | w ⁡ 0 = x
2 clwwlknon ⊢ y ClWWalksNOn ⁡ G N = w ∈ N ClWWalksN G | w ⁡ 0 = y
3 1 2 ineq12i ⊢ x ClWWalksNOn ⁡ G N ∩ y ClWWalksNOn ⁡ G N = w ∈ N ClWWalksN G | w ⁡ 0 = x ∩ w ∈ N ClWWalksN G | w ⁡ 0 = y
4 inrab ⊢ w ∈ N ClWWalksN G | w ⁡ 0 = x ∩ w ∈ N ClWWalksN G | w ⁡ 0 = y = w ∈ N ClWWalksN G | w ⁡ 0 = x ∧ w ⁡ 0 = y
5 eqtr2 ⊢ w ⁡ 0 = x ∧ w ⁡ 0 = y → x = y
6 5 con3i ⊢ ¬ x = y → ¬ w ⁡ 0 = x ∧ w ⁡ 0 = y
7 6 ralrimivw ⊢ ¬ x = y → ∀ w ∈ N ClWWalksN G ¬ w ⁡ 0 = x ∧ w ⁡ 0 = y
8 rabeq0 ⊢ w ∈ N ClWWalksN G | w ⁡ 0 = x ∧ w ⁡ 0 = y = ∅ ↔ ∀ w ∈ N ClWWalksN G ¬ w ⁡ 0 = x ∧ w ⁡ 0 = y
9 7 8 sylibr ⊢ ¬ x = y → w ∈ N ClWWalksN G | w ⁡ 0 = x ∧ w ⁡ 0 = y = ∅
10 4 9 syl5eq ⊢ ¬ x = y → w ∈ N ClWWalksN G | w ⁡ 0 = x ∩ w ∈ N ClWWalksN G | w ⁡ 0 = y = ∅
11 3 10 syl5eq ⊢ ¬ x = y → x ClWWalksNOn ⁡ G N ∩ y ClWWalksNOn ⁡ G N = ∅
12 11 orri ⊢ x = y ∨ x ClWWalksNOn ⁡ G N ∩ y ClWWalksNOn ⁡ G N = ∅
13 12 rgen2w ⊢ ∀ x ∈ V ∀ y ∈ V x = y ∨ x ClWWalksNOn ⁡ G N ∩ y ClWWalksNOn ⁡ G N = ∅
14 oveq1 ⊢ x = y → x ClWWalksNOn ⁡ G N = y ClWWalksNOn ⁡ G N
15 14 disjor ⊢ Disj x ∈ V x ClWWalksNOn ⁡ G N ↔ ∀ x ∈ V ∀ y ∈ V x = y ∨ x ClWWalksNOn ⁡ G N ∩ y ClWWalksNOn ⁡ G N = ∅
16 13 15 mpbir ⊢ Disj x ∈ V x ClWWalksNOn ⁡ G N