![]() |
Mathbox for Alexander van der Vekens |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > Mathboxes > usgrexmpl2nblem | Structured version Visualization version GIF version |
Description: Lemma for usgrexmpl2nb0 47766 etc. (Contributed by AV, 9-Aug-2025.) |
Ref | Expression |
---|---|
usgrexmpl2.v | ⊢ 𝑉 = (0...5) |
usgrexmpl2.e | ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 |
usgrexmpl2.g | ⊢ 𝐺 = 〈𝑉, 𝐸〉 |
Ref | Expression |
---|---|
usgrexmpl2nblem | ⊢ (𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | usgrexmpl2.v | . . 3 ⊢ 𝑉 = (0...5) | |
2 | usgrexmpl2.e | . . 3 ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 3} {3, 4} {4, 5} {0, 3} {0, 5}”〉 | |
3 | usgrexmpl2.g | . . 3 ⊢ 𝐺 = 〈𝑉, 𝐸〉 | |
4 | 1, 2, 3 | usgrexmpl2 47762 | . 2 ⊢ 𝐺 ∈ USGraph |
5 | 1, 2, 3 | usgrexmpl2vtx 47763 | . . . 4 ⊢ (Vtx‘𝐺) = ({0, 1, 2} ∪ {3, 4, 5}) |
6 | 5 | eqcomi 2743 | . . 3 ⊢ ({0, 1, 2} ∪ {3, 4, 5}) = (Vtx‘𝐺) |
7 | 1, 2, 3 | usgrexmpl2edg 47764 | . . . 4 ⊢ (Edg‘𝐺) = ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) |
8 | 7 | eqcomi 2743 | . . 3 ⊢ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}})) = (Edg‘𝐺) |
9 | 6, 8 | nbusgrvtx 29374 | . 2 ⊢ ((𝐺 ∈ USGraph ∧ 𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5})) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) |
10 | 4, 9 | mpan 689 | 1 ⊢ (𝐾 ∈ ({0, 1, 2} ∪ {3, 4, 5}) → (𝐺 NeighbVtx 𝐾) = {𝑛 ∈ ({0, 1, 2} ∪ {3, 4, 5}) ∣ {𝐾, 𝑛} ∈ ({{0, 3}} ∪ ({{0, 1}, {1, 2}, {2, 3}} ∪ {{3, 4}, {4, 5}, {0, 5}}))}) |
Colors of variables: wff setvar class |
Syntax hints: → wi 4 = wceq 1537 ∈ wcel 2103 {crab 3438 ∪ cun 3968 {csn 4648 {cpr 4650 {ctp 4652 〈cop 4654 ‘cfv 6572 (class class class)co 7445 0cc0 11180 1c1 11181 2c2 12344 3c3 12345 4c4 12346 5c5 12347 ...cfz 13563 〈“cs7 14891 Vtxcvtx 29022 Edgcedg 29073 USGraphcusgr 29175 NeighbVtx cnbgr 29358 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1793 ax-4 1807 ax-5 1909 ax-6 1967 ax-7 2007 ax-8 2105 ax-9 2113 ax-10 2136 ax-11 2153 ax-12 2173 ax-ext 2705 ax-rep 5306 ax-sep 5320 ax-nul 5327 ax-pow 5386 ax-pr 5450 ax-un 7766 ax-cnex 11236 ax-resscn 11237 ax-1cn 11238 ax-icn 11239 ax-addcl 11240 ax-addrcl 11241 ax-mulcl 11242 ax-mulrcl 11243 ax-mulcom 11244 ax-addass 11245 ax-mulass 11246 ax-distr 11247 ax-i2m1 11248 ax-1ne0 11249 ax-1rid 11250 ax-rnegex 11251 ax-rrecex 11252 ax-cnre 11253 ax-pre-lttri 11254 ax-pre-lttrn 11255 ax-pre-ltadd 11256 ax-pre-mulgt0 11257 |
This theorem depends on definitions: df-bi 207 df-an 396 df-or 847 df-3or 1088 df-3an 1089 df-tru 1540 df-fal 1550 df-ex 1778 df-nf 1782 df-sb 2065 df-mo 2537 df-eu 2566 df-clab 2712 df-cleq 2726 df-clel 2813 df-nfc 2890 df-ne 2943 df-nel 3049 df-ral 3064 df-rex 3073 df-reu 3384 df-rab 3439 df-v 3484 df-sbc 3799 df-csb 3916 df-dif 3973 df-un 3975 df-in 3977 df-ss 3987 df-pss 3990 df-nul 4348 df-if 4549 df-pw 4624 df-sn 4649 df-pr 4651 df-tp 4653 df-op 4655 df-uni 4932 df-int 4973 df-iun 5021 df-br 5170 df-opab 5232 df-mpt 5253 df-tr 5287 df-id 5597 df-eprel 5603 df-po 5611 df-so 5612 df-fr 5654 df-we 5656 df-xp 5705 df-rel 5706 df-cnv 5707 df-co 5708 df-dm 5709 df-rn 5710 df-res 5711 df-ima 5712 df-pred 6331 df-ord 6397 df-on 6398 df-lim 6399 df-suc 6400 df-iota 6524 df-fun 6574 df-fn 6575 df-f 6576 df-f1 6577 df-fo 6578 df-f1o 6579 df-fv 6580 df-riota 7401 df-ov 7448 df-oprab 7449 df-mpo 7450 df-om 7900 df-1st 8026 df-2nd 8027 df-frecs 8318 df-wrecs 8349 df-recs 8423 df-rdg 8462 df-1o 8518 df-2o 8519 df-oadd 8522 df-er 8759 df-en 9000 df-dom 9001 df-sdom 9002 df-fin 9003 df-dju 9966 df-card 10004 df-pnf 11322 df-mnf 11323 df-xr 11324 df-ltxr 11325 df-le 11326 df-sub 11518 df-neg 11519 df-nn 12290 df-2 12352 df-3 12353 df-4 12354 df-5 12355 df-6 12356 df-7 12357 df-n0 12550 df-xnn0 12622 df-z 12636 df-uz 12900 df-fz 13564 df-fzo 13708 df-hash 14376 df-word 14559 df-concat 14615 df-s1 14640 df-s2 14893 df-s3 14894 df-s4 14895 df-s5 14896 df-s6 14897 df-s7 14898 df-vtx 29024 df-iedg 29025 df-edg 29074 df-upgr 29108 df-umgr 29109 df-usgr 29177 df-nbgr 29359 |
This theorem is referenced by: usgrexmpl2nb0 47766 usgrexmpl2nb1 47767 usgrexmpl2nb2 47768 usgrexmpl2nb3 47769 usgrexmpl2nb4 47770 usgrexmpl2nb5 47771 |
Copyright terms: Public domain | W3C validator |