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

Theorem nb3grprlem2 28902
Description: Lemma 2 for nb3grpr 28903. (Contributed by Alexander van der Vekens, 17-Oct-2017.) (Revised by AV, 28-Oct-2020.) (Proof shortened by AV, 13-Feb-2022.)
Hypotheses
Ref Expression
nb3grpr.v 𝑉 = (Vtx‘𝐺)
nb3grpr.e 𝐸 = (Edg‘𝐺)
nb3grpr.g (𝜑𝐺 ∈ USGraph)
nb3grpr.t (𝜑𝑉 = {𝐴, 𝐵, 𝐶})
nb3grpr.s (𝜑 → (𝐴𝑋𝐵𝑌𝐶𝑍))
nb3grpr.n (𝜑 → (𝐴𝐵𝐴𝐶𝐵𝐶))
Assertion
Ref Expression
nb3grprlem2 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
Distinct variable groups:   𝑣,𝐴   𝑣,𝐵   𝑣,𝐶   𝑣,𝐸   𝑣,𝐺   𝑣,𝑉   𝜑,𝑣   𝑤,𝐴,𝑣   𝑤,𝐵   𝑤,𝐶   𝑤,𝐺   𝑤,𝑉
Allowed substitution hints:   𝜑(𝑤)   𝐸(𝑤)   𝑋(𝑤,𝑣)   𝑌(𝑤,𝑣)   𝑍(𝑤,𝑣)

Proof of Theorem nb3grprlem2
StepHypRef Expression
1 nb3grpr.s . . 3 (𝜑 → (𝐴𝑋𝐵𝑌𝐶𝑍))
2 sneq 4639 . . . . . 6 (𝑣 = 𝐴 → {𝑣} = {𝐴})
32difeq2d 4123 . . . . 5 (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
4 preq1 4738 . . . . . 6 (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
54eqeq2d 2742 . . . . 5 (𝑣 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
63, 5rexeqbidv 3342 . . . 4 (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
7 sneq 4639 . . . . . 6 (𝑣 = 𝐵 → {𝑣} = {𝐵})
87difeq2d 4123 . . . . 5 (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
9 preq1 4738 . . . . . 6 (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
109eqeq2d 2742 . . . . 5 (𝑣 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
118, 10rexeqbidv 3342 . . . 4 (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
12 sneq 4639 . . . . . 6 (𝑣 = 𝐶 → {𝑣} = {𝐶})
1312difeq2d 4123 . . . . 5 (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
14 preq1 4738 . . . . . 6 (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
1514eqeq2d 2742 . . . . 5 (𝑣 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
1613, 15rexeqbidv 3342 . . . 4 (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
176, 11, 16rextpg 4704 . . 3 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
181, 17syl 17 . 2 (𝜑 → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
19 nb3grpr.t . . . 4 (𝜑𝑉 = {𝐴, 𝐵, 𝐶})
20 nb3grpr.g . . . 4 (𝜑𝐺 ∈ USGraph)
2119, 20jca 511 . . 3 (𝜑 → (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph))
22 simpl 482 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → 𝑉 = {𝐴, 𝐵, 𝐶})
23 difeq1 4116 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2423adantr 480 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2524rexeqdv 3325 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
2622, 25rexeqbidv 3342 . . 3 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
2721, 26syl 17 . 2 (𝜑 → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
28 preq2 4739 . . . . . . . 8 (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
2928eqeq2d 2742 . . . . . . 7 (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵}))
30 preq2 4739 . . . . . . . 8 (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
3130eqeq2d 2742 . . . . . . 7 (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
3229, 31rexprg 4701 . . . . . 6 ((𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
33323adant1 1129 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
34 preq2 4739 . . . . . . . . 9 (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
3534eqeq2d 2742 . . . . . . . 8 (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
36 preq2 4739 . . . . . . . . 9 (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
3736eqeq2d 2742 . . . . . . . 8 (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
3835, 37rexprg 4701 . . . . . . 7 ((𝐶𝑍𝐴𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
3938ancoms 458 . . . . . 6 ((𝐴𝑋𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
40393adant2 1130 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
41 preq2 4739 . . . . . . . 8 (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
4241eqeq2d 2742 . . . . . . 7 (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
43 preq2 4739 . . . . . . . 8 (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
4443eqeq2d 2742 . . . . . . 7 (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
4542, 44rexprg 4701 . . . . . 6 ((𝐴𝑋𝐵𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
46453adant3 1131 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
4733, 40, 463orbi123d 1434 . . . 4 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
481, 47syl 17 . . 3 (𝜑 → ((∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
49 nb3grpr.n . . . 4 (𝜑 → (𝐴𝐵𝐴𝐶𝐵𝐶))
50 tprot 4754 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
5150a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
5251difeq1d 4122 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
53 necom 2993 . . . . . . . . 9 (𝐴𝐵𝐵𝐴)
54 necom 2993 . . . . . . . . 9 (𝐴𝐶𝐶𝐴)
55 diftpsn3 4806 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5653, 54, 55syl2anb 597 . . . . . . . 8 ((𝐴𝐵𝐴𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
57563adant3 1131 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5852, 57eqtrd 2771 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
5958rexeqdv 3325 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
60 tprot 4754 . . . . . . . . . 10 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
6160eqcomi 2740 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
6261a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
6362difeq1d 4122 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
64 necom 2993 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
6564anbi1i 623 . . . . . . . . . . 11 ((𝐵𝐶𝐴𝐵) ↔ (𝐶𝐵𝐴𝐵))
6665biimpi 215 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐵) → (𝐶𝐵𝐴𝐵))
6766ancoms 458 . . . . . . . . 9 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
68 diftpsn3 4806 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6967, 68syl 17 . . . . . . . 8 ((𝐴𝐵𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
70693adant2 1130 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
7163, 70eqtrd 2771 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
7271rexeqdv 3325 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
73 diftpsn3 4806 . . . . . . 7 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
74733adant1 1129 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
7574rexeqdv 3325 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
7659, 72, 753orbi123d 1434 . . . 4 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
7749, 76syl 17 . . 3 (𝜑 → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
78 prcom 4737 . . . . . . . 8 {𝐶, 𝐵} = {𝐵, 𝐶}
7978eqeq2i 2744 . . . . . . 7 ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
8079orbi2i 910 . . . . . 6 (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
81 oridm 902 . . . . . 6 (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
8280, 81bitr2i 275 . . . . 5 ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
8382a1i 11 . . . 4 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
84 nbgrnself2 28881 . . . . . . 7 𝐴 ∉ (𝐺 NeighbVtx 𝐴)
85 df-nel 3046 . . . . . . . 8 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) ↔ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴))
86 prid2g 4766 . . . . . . . . . . 11 (𝐴𝑋𝐴 ∈ {𝐵, 𝐴})
87863ad2ant1 1132 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐵, 𝐴})
88 eleq2 2821 . . . . . . . . . 10 ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
8987, 88syl5ibrcom 246 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
9089con3rr3 155 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
9185, 90sylbi 216 . . . . . . 7 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
9284, 1, 91mpsyl 68 . . . . . 6 (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})
93 biorf 934 . . . . . . 7 (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})))
94 orcom 867 . . . . . . 7 (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
9593, 94bitrdi 286 . . . . . 6 (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
9692, 95syl 17 . . . . 5 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
97 prid2g 4766 . . . . . . . . . . 11 (𝐴𝑋𝐴 ∈ {𝐶, 𝐴})
98973ad2ant1 1132 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐶, 𝐴})
99 eleq2 2821 . . . . . . . . . 10 ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
10098, 99syl5ibrcom 246 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
101100con3rr3 155 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
10285, 101sylbi 216 . . . . . . 7 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
10384, 1, 102mpsyl 68 . . . . . 6 (𝜑 → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴})
104 biorf 934 . . . . . 6 (¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
105103, 104syl 17 . . . . 5 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
10696, 105orbi12d 916 . . . 4 (𝜑 → (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
107 prid1g 4765 . . . . . . . . . . . . 13 (𝐴𝑋𝐴 ∈ {𝐴, 𝐵})
1081073ad2ant1 1132 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐵})
109 eleq2 2821 . . . . . . . . . . . 12 ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
110108, 109syl5ibrcom 246 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
111110con3dimp 408 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵})
112 prid1g 4765 . . . . . . . . . . . . 13 (𝐴𝑋𝐴 ∈ {𝐴, 𝐶})
1131123ad2ant1 1132 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐶})
114 eleq2 2821 . . . . . . . . . . . 12 ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
115113, 114syl5ibrcom 246 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
116115con3dimp 408 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})
117111, 116jca 511 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
118117expcom 413 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
11985, 118sylbi 216 . . . . . . 7 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
12084, 1, 119mpsyl 68 . . . . . 6 (𝜑 → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
121 ioran 981 . . . . . 6 (¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ↔ (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
122120, 121sylibr 233 . . . . 5 (𝜑 → ¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
1231223bior1fd 1474 . . . 4 (𝜑 → ((((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
12483, 106, 1233bitrd 304 . . 3 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
12548, 77, 1243bitr4rd 311 . 2 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
12618, 27, 1253bitr4rd 311 1 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 205  wa 395  wo 844  w3o 1085  w3a 1086   = wceq 1540  wcel 2105  wne 2939  wnel 3045  wrex 3069  cdif 3946  {csn 4629  {cpr 4631  {ctp 4633  cfv 6544  (class class class)co 7412  Vtxcvtx 28520  Edgcedg 28571  USGraphcusgr 28673   NeighbVtx cnbgr 28853
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2153  ax-12 2170  ax-ext 2702  ax-sep 5300  ax-nul 5307  ax-pr 5428  ax-un 7728
This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3or 1087  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-nf 1785  df-sb 2067  df-mo 2533  df-eu 2562  df-clab 2709  df-cleq 2723  df-clel 2809  df-nfc 2884  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rab 3432  df-v 3475  df-sbc 3779  df-csb 3895  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-tp 4634  df-op 4636  df-uni 4910  df-iun 5000  df-br 5150  df-opab 5212  df-mpt 5233  df-id 5575  df-xp 5683  df-rel 5684  df-cnv 5685  df-co 5686  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690  df-iota 6496  df-fun 6546  df-fv 6552  df-ov 7415  df-oprab 7416  df-mpo 7417  df-1st 7978  df-2nd 7979  df-nbgr 28854
This theorem is referenced by:  nb3grpr  28903
  Copyright terms: Public domain W3C validator