MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nb3graprlem2 Structured version   Visualization version   GIF version

Theorem nb3graprlem2 25981
Description: Lemma 2 for nb3grapr 25982. (Contributed by Alexander van der Vekens, 17-Oct-2017.)
Assertion
Ref Expression
nb3graprlem2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
Distinct variable groups:   𝑣,𝐸,𝑤   𝑣,𝑉,𝑤   𝑣,𝐴,𝑤   𝑣,𝐵,𝑤   𝑣,𝐶,𝑤
Allowed substitution hints:   𝑋(𝑤,𝑣)   𝑌(𝑤,𝑣)   𝑍(𝑤,𝑣)

Proof of Theorem nb3graprlem2
StepHypRef Expression
1 sneq 4135 . . . . . 6 (𝑣 = 𝐴 → {𝑣} = {𝐴})
21difeq2d 3690 . . . . 5 (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
3 preq1 4212 . . . . . 6 (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
43eqeq2d 2620 . . . . 5 (𝑣 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
52, 4rexeqbidv 3130 . . . 4 (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
6 sneq 4135 . . . . . 6 (𝑣 = 𝐵 → {𝑣} = {𝐵})
76difeq2d 3690 . . . . 5 (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
8 preq1 4212 . . . . . 6 (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
98eqeq2d 2620 . . . . 5 (𝑣 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
107, 9rexeqbidv 3130 . . . 4 (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
11 sneq 4135 . . . . . 6 (𝑣 = 𝐶 → {𝑣} = {𝐶})
1211difeq2d 3690 . . . . 5 (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
13 preq1 4212 . . . . . 6 (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
1413eqeq2d 2620 . . . . 5 (𝑣 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
1512, 14rexeqbidv 3130 . . . 4 (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
165, 10, 15rextpg 4184 . . 3 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
17163ad2ant1 1075 . 2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
18 simpl 472 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → 𝑉 = {𝐴, 𝐵, 𝐶})
19 difeq1 3683 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2019adantr 480 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2120rexeqdv 3122 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
2218, 21rexeqbidv 3130 . . 3 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
23223ad2ant2 1076 . 2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
24 preq2 4213 . . . . . . . 8 (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
2524eqeq2d 2620 . . . . . . 7 (𝑤 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵}))
26 preq2 4213 . . . . . . . 8 (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
2726eqeq2d 2620 . . . . . . 7 (𝑤 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
2825, 27rexprg 4182 . . . . . 6 ((𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
29283adant1 1072 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
30 preq2 4213 . . . . . . . . 9 (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
3130eqeq2d 2620 . . . . . . . 8 (𝑤 = 𝐶 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}))
32 preq2 4213 . . . . . . . . 9 (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
3332eqeq2d 2620 . . . . . . . 8 (𝑤 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
3431, 33rexprg 4182 . . . . . . 7 ((𝐶𝑍𝐴𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
3534ancoms 468 . . . . . 6 ((𝐴𝑋𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
36353adant2 1073 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
37 preq2 4213 . . . . . . . 8 (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
3837eqeq2d 2620 . . . . . . 7 (𝑤 = 𝐴 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
39 preq2 4213 . . . . . . . 8 (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
4039eqeq2d 2620 . . . . . . 7 (𝑤 = 𝐵 → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))
4138, 40rexprg 4182 . . . . . 6 ((𝐴𝑋𝐵𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
42413adant3 1074 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
4329, 36, 423orbi123d 1390 . . . 4 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
44433ad2ant1 1075 . . 3 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
45 tprot 4228 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
4645a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
4746difeq1d 3689 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
48 necom 2835 . . . . . . . . 9 (𝐴𝐵𝐵𝐴)
49 necom 2835 . . . . . . . . 9 (𝐴𝐶𝐶𝐴)
50 diftpsn3 4273 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5148, 49, 50syl2anb 495 . . . . . . . 8 ((𝐴𝐵𝐴𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
52513adant3 1074 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5347, 52eqtrd 2644 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
5453rexeqdv 3122 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤}))
55 tprot 4228 . . . . . . . . . 10 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
5655eqcomi 2619 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
5756a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
5857difeq1d 3689 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
59 necom 2835 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
6059anbi1i 727 . . . . . . . . . . 11 ((𝐵𝐶𝐴𝐵) ↔ (𝐶𝐵𝐴𝐵))
6160biimpi 205 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐵) → (𝐶𝐵𝐴𝐵))
6261ancoms 468 . . . . . . . . 9 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
63 diftpsn3 4273 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6462, 63syl 17 . . . . . . . 8 ((𝐴𝐵𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
65643adant2 1073 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6658, 65eqtrd 2644 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
6766rexeqdv 3122 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤}))
68 diftpsn3 4273 . . . . . . 7 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
69683adant1 1072 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
7069rexeqdv 3122 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}))
7154, 67, 703orbi123d 1390 . . . 4 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
72713ad2ant3 1077 . . 3 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
73 prcom 4211 . . . . . . . 8 {𝐶, 𝐵} = {𝐵, 𝐶}
7473eqeq2i 2622 . . . . . . 7 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})
7574orbi2i 540 . . . . . 6 (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}))
76 oridm 535 . . . . . 6 (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}) ↔ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})
7775, 76bitr2i 264 . . . . 5 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))
7877a1i 11 . . . 4 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
79 nbgranself2 25965 . . . . . . . . . 10 (𝑉 USGrph 𝐸𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴))
80 df-nel 2783 . . . . . . . . . . 11 (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴))
81 prid2g 4240 . . . . . . . . . . . . . 14 (𝐴𝑋𝐴 ∈ {𝐵, 𝐴})
82813ad2ant1 1075 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐵, 𝐴})
83 eleq2 2677 . . . . . . . . . . . . 13 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
8482, 83syl5ibrcom 236 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
8584con3rr3 150 . . . . . . . . . . 11 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
8680, 85sylbi 206 . . . . . . . . . 10 (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
8779, 86syl 17 . . . . . . . . 9 (𝑉 USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
8887adantl 481 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
8988impcom 445 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})
90893adant3 1074 . . . . . 6 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})
91 biorf 419 . . . . . . 7 (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶})))
92 orcom 401 . . . . . . 7 (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶}) ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}))
9391, 92syl6bb 275 . . . . . 6 (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
9490, 93syl 17 . . . . 5 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴})))
95 prid2g 4240 . . . . . . . . . . . . . 14 (𝐴𝑋𝐴 ∈ {𝐶, 𝐴})
96953ad2ant1 1075 . . . . . . . . . . . . 13 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐶, 𝐴})
97 eleq2 2677 . . . . . . . . . . . . 13 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
9896, 97syl5ibrcom 236 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
9998con3rr3 150 . . . . . . . . . . 11 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
10080, 99sylbi 206 . . . . . . . . . 10 (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
10179, 100syl 17 . . . . . . . . 9 (𝑉 USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
102101adantl 481 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴}))
103102impcom 445 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴})
1041033adant3 1074 . . . . . 6 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴})
105 biorf 419 . . . . . 6 (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
106104, 105syl 17 . . . . 5 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵} ↔ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})))
10794, 106orbi12d 742 . . . 4 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
108 prid1g 4239 . . . . . . . . . . . . . . . 16 (𝐴𝑋𝐴 ∈ {𝐴, 𝐵})
1091083ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐵})
110 eleq2 2677 . . . . . . . . . . . . . . 15 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
111109, 110syl5ibrcom 236 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
112111con3dimp 456 . . . . . . . . . . . . 13 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵})
113 prid1g 4239 . . . . . . . . . . . . . . . 16 (𝐴𝑋𝐴 ∈ {𝐴, 𝐶})
1141133ad2ant1 1075 . . . . . . . . . . . . . . 15 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐶})
115 eleq2 2677 . . . . . . . . . . . . . . 15 ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
116114, 115syl5ibrcom 236 . . . . . . . . . . . . . 14 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)))
117116con3dimp 456 . . . . . . . . . . . . 13 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})
118112, 117jca 553 . . . . . . . . . . . 12 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
119118expcom 450 . . . . . . . . . . 11 𝐴 ∈ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
12080, 119sylbi 206 . . . . . . . . . 10 (𝐴 ∉ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
12179, 120syl 17 . . . . . . . . 9 (𝑉 USGrph 𝐸 → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
122121adantl 481 . . . . . . . 8 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶})))
123122impcom 445 . . . . . . 7 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
1241233adant3 1074 . . . . . 6 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
125 ioran 510 . . . . . 6 (¬ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ↔ (¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∧ ¬ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
126124, 125sylibr 223 . . . . 5 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ¬ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}))
1271263bior1fd 1430 . . . 4 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵})) ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
12878, 107, 1273bitrd 293 . . 3 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ (((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐵} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝐶}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐴}) ∨ ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐴} ∨ (⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝐵}))))
12944, 72, 1283bitr4rd 300 . 2 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐶, 𝑤})))
13017, 23, 1293bitr4rd 300 1 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝑉 USGrph 𝐸) ∧ (𝐴𝐵𝐴𝐶𝐵𝐶)) → ((⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(⟨𝑉, 𝐸⟩ Neighbors 𝐴) = {𝑣, 𝑤}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 195  wo 382  wa 383  w3o 1030  w3a 1031   = wceq 1475  wcel 1977  wne 2780  wnel 2781  wrex 2897  cdif 3537  {csn 4125  {cpr 4127  {ctp 4129  cop 4131   class class class wbr 4583  (class class class)co 6549   USGrph cusg 25859   Neighbors cnbgra 25946
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-8 1979  ax-9 1986  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-rep 4699  ax-sep 4709  ax-nul 4717  ax-pow 4769  ax-pr 4833  ax-un 6847  ax-cnex 9871  ax-resscn 9872  ax-1cn 9873  ax-icn 9874  ax-addcl 9875  ax-addrcl 9876  ax-mulcl 9877  ax-mulrcl 9878  ax-mulcom 9879  ax-addass 9880  ax-mulass 9881  ax-distr 9882  ax-i2m1 9883  ax-1ne0 9884  ax-1rid 9885  ax-rnegex 9886  ax-rrecex 9887  ax-cnre 9888  ax-pre-lttri 9889  ax-pre-lttrn 9890  ax-pre-ltadd 9891  ax-pre-mulgt0 9892
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3or 1032  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-eu 2462  df-mo 2463  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-nel 2783  df-ral 2901  df-rex 2902  df-reu 2903  df-rmo 2904  df-rab 2905  df-v 3175  df-sbc 3403  df-csb 3500  df-dif 3543  df-un 3545  df-in 3547  df-ss 3554  df-pss 3556  df-nul 3875  df-if 4037  df-pw 4110  df-sn 4126  df-pr 4128  df-tp 4130  df-op 4132  df-uni 4373  df-int 4411  df-iun 4457  df-br 4584  df-opab 4644  df-mpt 4645  df-tr 4681  df-eprel 4949  df-id 4953  df-po 4959  df-so 4960  df-fr 4997  df-we 4999  df-xp 5044  df-rel 5045  df-cnv 5046  df-co 5047  df-dm 5048  df-rn 5049  df-res 5050  df-ima 5051  df-pred 5597  df-ord 5643  df-on 5644  df-lim 5645  df-suc 5646  df-iota 5768  df-fun 5806  df-fn 5807  df-f 5808  df-f1 5809  df-fo 5810  df-f1o 5811  df-fv 5812  df-riota 6511  df-ov 6552  df-oprab 6553  df-mpt2 6554  df-om 6958  df-1st 7059  df-2nd 7060  df-wrecs 7294  df-recs 7355  df-rdg 7393  df-1o 7447  df-oadd 7451  df-er 7629  df-en 7842  df-dom 7843  df-sdom 7844  df-fin 7845  df-card 8648  df-cda 8873  df-pnf 9955  df-mnf 9956  df-xr 9957  df-ltxr 9958  df-le 9959  df-sub 10147  df-neg 10148  df-nn 10898  df-2 10956  df-n0 11170  df-z 11255  df-uz 11564  df-fz 12198  df-hash 12980  df-usgra 25862  df-nbgra 25949
This theorem is referenced by:  nb3grapr  25982
  Copyright terms: Public domain W3C validator