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

Theorem nb3grprlem2 27160
Description: Lemma 2 for nb3grpr 27161. (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 4558 . . . . . 6 (𝑣 = 𝐴 → {𝑣} = {𝐴})
32difeq2d 4083 . . . . 5 (𝑣 = 𝐴 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐴}))
4 preq1 4650 . . . . . 6 (𝑣 = 𝐴 → {𝑣, 𝑤} = {𝐴, 𝑤})
54eqeq2d 2835 . . . . 5 (𝑣 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
63, 5rexeqbidv 3393 . . . 4 (𝑣 = 𝐴 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
7 sneq 4558 . . . . . 6 (𝑣 = 𝐵 → {𝑣} = {𝐵})
87difeq2d 4083 . . . . 5 (𝑣 = 𝐵 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐵}))
9 preq1 4650 . . . . . 6 (𝑣 = 𝐵 → {𝑣, 𝑤} = {𝐵, 𝑤})
109eqeq2d 2835 . . . . 5 (𝑣 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
118, 10rexeqbidv 3393 . . . 4 (𝑣 = 𝐵 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
12 sneq 4558 . . . . . 6 (𝑣 = 𝐶 → {𝑣} = {𝐶})
1312difeq2d 4083 . . . . 5 (𝑣 = 𝐶 → ({𝐴, 𝐵, 𝐶} ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝐶}))
14 preq1 4650 . . . . . 6 (𝑣 = 𝐶 → {𝑣, 𝑤} = {𝐶, 𝑤})
1514eqeq2d 2835 . . . . 5 (𝑣 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
1613, 15rexeqbidv 3393 . . . 4 (𝑣 = 𝐶 → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
176, 11, 16rextpg 4616 . . 3 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
181, 17syl 17 . 2 (𝜑 → (∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
19 nb3grpr.t . . . 4 (𝜑𝑉 = {𝐴, 𝐵, 𝐶})
20 nb3grpr.g . . . 4 (𝜑𝐺 ∈ USGraph)
2119, 20jca 515 . . 3 (𝜑 → (𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph))
22 simpl 486 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → 𝑉 = {𝐴, 𝐵, 𝐶})
23 difeq1 4076 . . . . . 6 (𝑉 = {𝐴, 𝐵, 𝐶} → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2423adantr 484 . . . . 5 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (𝑉 ∖ {𝑣}) = ({𝐴, 𝐵, 𝐶} ∖ {𝑣}))
2524rexeqdv 3403 . . . 4 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
2622, 25rexeqbidv 3393 . . 3 ((𝑉 = {𝐴, 𝐵, 𝐶} ∧ 𝐺 ∈ USGraph) → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
2721, 26syl 17 . 2 (𝜑 → (∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤} ↔ ∃𝑣 ∈ {𝐴, 𝐵, 𝐶}∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
28 preq2 4651 . . . . . . . 8 (𝑤 = 𝐵 → {𝐴, 𝑤} = {𝐴, 𝐵})
2928eqeq2d 2835 . . . . . . 7 (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵}))
30 preq2 4651 . . . . . . . 8 (𝑤 = 𝐶 → {𝐴, 𝑤} = {𝐴, 𝐶})
3130eqeq2d 2835 . . . . . . 7 (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
3229, 31rexprg 4614 . . . . . 6 ((𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
33323adant1 1127 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
34 preq2 4651 . . . . . . . . 9 (𝑤 = 𝐶 → {𝐵, 𝑤} = {𝐵, 𝐶})
3534eqeq2d 2835 . . . . . . . 8 (𝑤 = 𝐶 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
36 preq2 4651 . . . . . . . . 9 (𝑤 = 𝐴 → {𝐵, 𝑤} = {𝐵, 𝐴})
3736eqeq2d 2835 . . . . . . . 8 (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
3835, 37rexprg 4614 . . . . . . 7 ((𝐶𝑍𝐴𝑋) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
3938ancoms 462 . . . . . 6 ((𝐴𝑋𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
40393adant2 1128 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
41 preq2 4651 . . . . . . . 8 (𝑤 = 𝐴 → {𝐶, 𝑤} = {𝐶, 𝐴})
4241eqeq2d 2835 . . . . . . 7 (𝑤 = 𝐴 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
43 preq2 4651 . . . . . . . 8 (𝑤 = 𝐵 → {𝐶, 𝑤} = {𝐶, 𝐵})
4443eqeq2d 2835 . . . . . . 7 (𝑤 = 𝐵 → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
4542, 44rexprg 4614 . . . . . 6 ((𝐴𝑋𝐵𝑌) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
46453adant3 1129 . . . . 5 ((𝐴𝑋𝐵𝑌𝐶𝑍) → (∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
4733, 40, 463orbi123d 1432 . . . 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 4666 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴}
5150a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐵, 𝐶, 𝐴})
5251difeq1d 4082 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = ({𝐵, 𝐶, 𝐴} ∖ {𝐴}))
53 necom 3066 . . . . . . . . 9 (𝐴𝐵𝐵𝐴)
54 necom 3066 . . . . . . . . 9 (𝐴𝐶𝐶𝐴)
55 diftpsn3 4716 . . . . . . . . 9 ((𝐵𝐴𝐶𝐴) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5653, 54, 55syl2anb 600 . . . . . . . 8 ((𝐴𝐵𝐴𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
57563adant3 1129 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐵, 𝐶, 𝐴} ∖ {𝐴}) = {𝐵, 𝐶})
5852, 57eqtrd 2859 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐴}) = {𝐵, 𝐶})
5958rexeqdv 3403 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ↔ ∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤}))
60 tprot 4666 . . . . . . . . . 10 {𝐶, 𝐴, 𝐵} = {𝐴, 𝐵, 𝐶}
6160eqcomi 2833 . . . . . . . . 9 {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵}
6261a1i 11 . . . . . . . 8 ((𝐴𝐵𝐴𝐶𝐵𝐶) → {𝐴, 𝐵, 𝐶} = {𝐶, 𝐴, 𝐵})
6362difeq1d 4082 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = ({𝐶, 𝐴, 𝐵} ∖ {𝐵}))
64 necom 3066 . . . . . . . . . . . 12 (𝐵𝐶𝐶𝐵)
6564anbi1i 626 . . . . . . . . . . 11 ((𝐵𝐶𝐴𝐵) ↔ (𝐶𝐵𝐴𝐵))
6665biimpi 219 . . . . . . . . . 10 ((𝐵𝐶𝐴𝐵) → (𝐶𝐵𝐴𝐵))
6766ancoms 462 . . . . . . . . 9 ((𝐴𝐵𝐵𝐶) → (𝐶𝐵𝐴𝐵))
68 diftpsn3 4716 . . . . . . . . 9 ((𝐶𝐵𝐴𝐵) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
6967, 68syl 17 . . . . . . . 8 ((𝐴𝐵𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
70693adant2 1128 . . . . . . 7 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐶, 𝐴, 𝐵} ∖ {𝐵}) = {𝐶, 𝐴})
7163, 70eqtrd 2859 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐵}) = {𝐶, 𝐴})
7271rexeqdv 3403 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ↔ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤}))
73 diftpsn3 4716 . . . . . . 7 ((𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
74733adant1 1127 . . . . . 6 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ({𝐴, 𝐵, 𝐶} ∖ {𝐶}) = {𝐴, 𝐵})
7574rexeqdv 3403 . . . . 5 ((𝐴𝐵𝐴𝐶𝐵𝐶) → (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤} ↔ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}))
7659, 72, 753orbi123d 1432 . . . 4 ((𝐴𝐵𝐴𝐶𝐵𝐶) → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
7749, 76syl 17 . . 3 (𝜑 → ((∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤}) ↔ (∃𝑤 ∈ {𝐵, 𝐶} (𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ {𝐶, 𝐴} (𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ {𝐴, 𝐵} (𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
78 prcom 4649 . . . . . . . 8 {𝐶, 𝐵} = {𝐵, 𝐶}
7978eqeq2i 2837 . . . . . . 7 ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵} ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
8079orbi2i 910 . . . . . 6 (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}) ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}))
81 oridm 902 . . . . . 6 (((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶}) ↔ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶})
8280, 81bitr2i 279 . . . . 5 ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))
8382a1i 11 . . . 4 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})))
84 nbgrnself2 27139 . . . . . . 7 𝐴 ∉ (𝐺 NeighbVtx 𝐴)
85 df-nel 3118 . . . . . . . 8 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) ↔ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴))
86 prid2g 4678 . . . . . . . . . . 11 (𝐴𝑋𝐴 ∈ {𝐵, 𝐴})
87863ad2ant1 1130 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐵, 𝐴})
88 eleq2 2904 . . . . . . . . . 10 ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐵, 𝐴}))
8987, 88syl5ibrcom 250 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
9089con3rr3 158 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}))
9185, 90sylbi 220 . . . . . . 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, 94syl6bb 290 . . . . . 6 (¬ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴} → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
9692, 95syl 17 . . . . 5 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴})))
97 prid2g 4678 . . . . . . . . . . 11 (𝐴𝑋𝐴 ∈ {𝐶, 𝐴})
98973ad2ant1 1130 . . . . . . . . . 10 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐶, 𝐴})
99 eleq2 2904 . . . . . . . . . 10 ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐶, 𝐴}))
10098, 99syl5ibrcom 250 . . . . . . . . 9 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
101100con3rr3 158 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴}))
10285, 101sylbi 220 . . . . . . 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 4677 . . . . . . . . . . . . 13 (𝐴𝑋𝐴 ∈ {𝐴, 𝐵})
1081073ad2ant1 1130 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐵})
109 eleq2 2904 . . . . . . . . . . . 12 ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐵}))
110108, 109syl5ibrcom 250 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
111110con3dimp 412 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵})
112 prid1g 4677 . . . . . . . . . . . . 13 (𝐴𝑋𝐴 ∈ {𝐴, 𝐶})
1131123ad2ant1 1130 . . . . . . . . . . . 12 ((𝐴𝑋𝐵𝑌𝐶𝑍) → 𝐴 ∈ {𝐴, 𝐶})
114 eleq2 2904 . . . . . . . . . . . 12 ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → (𝐴 ∈ (𝐺 NeighbVtx 𝐴) ↔ 𝐴 ∈ {𝐴, 𝐶}))
115113, 114syl5ibrcom 250 . . . . . . . . . . 11 ((𝐴𝑋𝐵𝑌𝐶𝑍) → ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶} → 𝐴 ∈ (𝐺 NeighbVtx 𝐴)))
116115con3dimp 412 . . . . . . . . . 10 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})
117111, 116jca 515 . . . . . . . . 9 (((𝐴𝑋𝐵𝑌𝐶𝑍) ∧ ¬ 𝐴 ∈ (𝐺 NeighbVtx 𝐴)) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
118117expcom 417 . . . . . . . 8 𝐴 ∈ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
11985, 118sylbi 220 . . . . . . 7 (𝐴 ∉ (𝐺 NeighbVtx 𝐴) → ((𝐴𝑋𝐵𝑌𝐶𝑍) → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶})))
12084, 1, 119mpsyl 68 . . . . . 6 (𝜑 → (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
121 ioran 981 . . . . . 6 (¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ↔ (¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∧ ¬ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
122120, 121sylibr 237 . . . . 5 (𝜑 → ¬ ((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}))
1231223bior1fd 1472 . . . 4 (𝜑 → ((((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵})) ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
12483, 106, 1233bitrd 308 . . 3 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (((𝐺 NeighbVtx 𝐴) = {𝐴, 𝐵} ∨ (𝐺 NeighbVtx 𝐴) = {𝐴, 𝐶}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ∨ (𝐺 NeighbVtx 𝐴) = {𝐵, 𝐴}) ∨ ((𝐺 NeighbVtx 𝐴) = {𝐶, 𝐴} ∨ (𝐺 NeighbVtx 𝐴) = {𝐶, 𝐵}))))
12548, 77, 1243bitr4rd 315 . 2 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ (∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐴})(𝐺 NeighbVtx 𝐴) = {𝐴, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐵})(𝐺 NeighbVtx 𝐴) = {𝐵, 𝑤} ∨ ∃𝑤 ∈ ({𝐴, 𝐵, 𝐶} ∖ {𝐶})(𝐺 NeighbVtx 𝐴) = {𝐶, 𝑤})))
12618, 27, 1253bitr4rd 315 1 (𝜑 → ((𝐺 NeighbVtx 𝐴) = {𝐵, 𝐶} ↔ ∃𝑣𝑉𝑤 ∈ (𝑉 ∖ {𝑣})(𝐺 NeighbVtx 𝐴) = {𝑣, 𝑤}))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 209  wa 399  wo 844  w3o 1083  w3a 1084   = wceq 1538  wcel 2115  wne 3013  wnel 3117  wrex 3133  cdif 3915  {csn 4548  {cpr 4550  {ctp 4552  cfv 6336  (class class class)co 7138  Vtxcvtx 26778  Edgcedg 26829  USGraphcusgr 26931   NeighbVtx cnbgr 27111
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796  ax-sep 5184  ax-nul 5191  ax-pow 5247  ax-pr 5311  ax-un 7444
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2071  df-mo 2624  df-eu 2655  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-ne 3014  df-nel 3118  df-ral 3137  df-rex 3138  df-rab 3141  df-v 3481  df-sbc 3758  df-csb 3866  df-dif 3921  df-un 3923  df-in 3925  df-ss 3935  df-nul 4275  df-if 4449  df-sn 4549  df-pr 4551  df-tp 4553  df-op 4555  df-uni 4820  df-iun 4902  df-br 5048  df-opab 5110  df-mpt 5128  df-id 5441  df-xp 5542  df-rel 5543  df-cnv 5544  df-co 5545  df-dm 5546  df-rn 5547  df-res 5548  df-ima 5549  df-iota 6295  df-fun 6338  df-fv 6344  df-ov 7141  df-oprab 7142  df-mpo 7143  df-1st 7672  df-2nd 7673  df-nbgr 27112
This theorem is referenced by:  nb3grpr  27161
  Copyright terms: Public domain W3C validator