![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > usgrexmpllem | Structured version Visualization version GIF version |
Description: Lemma for usgrexmpl 26763. (Contributed by AV, 21-Oct-2020.) |
Ref | Expression |
---|---|
usgrexmpl.v | ⊢ 𝑉 = (0...4) |
usgrexmpl.e | ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 |
usgrexmpl.g | ⊢ 𝐺 = 〈𝑉, 𝐸〉 |
Ref | Expression |
---|---|
usgrexmpllem | ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | usgrexmpl.v | . . . 4 ⊢ 𝑉 = (0...4) | |
2 | 1 | ovexi 7015 | . . 3 ⊢ 𝑉 ∈ V |
3 | usgrexmpl.e | . . . 4 ⊢ 𝐸 = 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 | |
4 | s4cli 14112 | . . . . 5 ⊢ 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 ∈ Word V | |
5 | 4 | elexi 3436 | . . . 4 ⊢ 〈“{0, 1} {1, 2} {2, 0} {0, 3}”〉 ∈ V |
6 | 3, 5 | eqeltri 2864 | . . 3 ⊢ 𝐸 ∈ V |
7 | opvtxfv 26507 | . . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (Vtx‘〈𝑉, 𝐸〉) = 𝑉) | |
8 | opiedgfv 26510 | . . . 4 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → (iEdg‘〈𝑉, 𝐸〉) = 𝐸) | |
9 | 7, 8 | jca 504 | . . 3 ⊢ ((𝑉 ∈ V ∧ 𝐸 ∈ V) → ((Vtx‘〈𝑉, 𝐸〉) = 𝑉 ∧ (iEdg‘〈𝑉, 𝐸〉) = 𝐸)) |
10 | 2, 6, 9 | mp2an 680 | . 2 ⊢ ((Vtx‘〈𝑉, 𝐸〉) = 𝑉 ∧ (iEdg‘〈𝑉, 𝐸〉) = 𝐸) |
11 | usgrexmpl.g | . . . . 5 ⊢ 𝐺 = 〈𝑉, 𝐸〉 | |
12 | 11 | fveq2i 6507 | . . . 4 ⊢ (Vtx‘𝐺) = (Vtx‘〈𝑉, 𝐸〉) |
13 | 12 | eqeq1i 2785 | . . 3 ⊢ ((Vtx‘𝐺) = 𝑉 ↔ (Vtx‘〈𝑉, 𝐸〉) = 𝑉) |
14 | 11 | fveq2i 6507 | . . . 4 ⊢ (iEdg‘𝐺) = (iEdg‘〈𝑉, 𝐸〉) |
15 | 14 | eqeq1i 2785 | . . 3 ⊢ ((iEdg‘𝐺) = 𝐸 ↔ (iEdg‘〈𝑉, 𝐸〉) = 𝐸) |
16 | 13, 15 | anbi12i 618 | . 2 ⊢ (((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸) ↔ ((Vtx‘〈𝑉, 𝐸〉) = 𝑉 ∧ (iEdg‘〈𝑉, 𝐸〉) = 𝐸)) |
17 | 10, 16 | mpbir 223 | 1 ⊢ ((Vtx‘𝐺) = 𝑉 ∧ (iEdg‘𝐺) = 𝐸) |
Colors of variables: wff setvar class |
Syntax hints: ∧ wa 387 = wceq 1508 ∈ wcel 2051 Vcvv 3417 {cpr 4446 〈cop 4450 ‘cfv 6193 (class class class)co 6982 0cc0 10341 1c1 10342 2c2 11501 3c3 11502 4c4 11503 ...cfz 12714 Word cword 13678 〈“cs4 14073 Vtxcvtx 26499 iEdgciedg 26500 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1759 ax-4 1773 ax-5 1870 ax-6 1929 ax-7 1966 ax-8 2053 ax-9 2060 ax-10 2080 ax-11 2094 ax-12 2107 ax-13 2302 ax-ext 2752 ax-rep 5053 ax-sep 5064 ax-nul 5071 ax-pow 5123 ax-pr 5190 ax-un 7285 ax-cnex 10397 ax-resscn 10398 ax-1cn 10399 ax-icn 10400 ax-addcl 10401 ax-addrcl 10402 ax-mulcl 10403 ax-mulrcl 10404 ax-mulcom 10405 ax-addass 10406 ax-mulass 10407 ax-distr 10408 ax-i2m1 10409 ax-1ne0 10410 ax-1rid 10411 ax-rnegex 10412 ax-rrecex 10413 ax-cnre 10414 ax-pre-lttri 10415 ax-pre-lttrn 10416 ax-pre-ltadd 10417 ax-pre-mulgt0 10418 |
This theorem depends on definitions: df-bi 199 df-an 388 df-or 835 df-3or 1070 df-3an 1071 df-tru 1511 df-ex 1744 df-nf 1748 df-sb 2017 df-mo 2551 df-eu 2589 df-clab 2761 df-cleq 2773 df-clel 2848 df-nfc 2920 df-ne 2970 df-nel 3076 df-ral 3095 df-rex 3096 df-reu 3097 df-rab 3099 df-v 3419 df-sbc 3684 df-csb 3789 df-dif 3834 df-un 3836 df-in 3838 df-ss 3845 df-pss 3847 df-nul 4182 df-if 4354 df-pw 4427 df-sn 4445 df-pr 4447 df-tp 4449 df-op 4451 df-uni 4718 df-int 4755 df-iun 4799 df-br 4935 df-opab 4997 df-mpt 5014 df-tr 5036 df-id 5316 df-eprel 5321 df-po 5330 df-so 5331 df-fr 5370 df-we 5372 df-xp 5417 df-rel 5418 df-cnv 5419 df-co 5420 df-dm 5421 df-rn 5422 df-res 5423 df-ima 5424 df-pred 5991 df-ord 6037 df-on 6038 df-lim 6039 df-suc 6040 df-iota 6157 df-fun 6195 df-fn 6196 df-f 6197 df-f1 6198 df-fo 6199 df-f1o 6200 df-fv 6201 df-riota 6943 df-ov 6985 df-oprab 6986 df-mpo 6987 df-om 7403 df-1st 7507 df-2nd 7508 df-wrecs 7756 df-recs 7818 df-rdg 7856 df-1o 7911 df-oadd 7915 df-er 8095 df-en 8313 df-dom 8314 df-sdom 8315 df-fin 8316 df-card 9168 df-pnf 10482 df-mnf 10483 df-xr 10484 df-ltxr 10485 df-le 10486 df-sub 10678 df-neg 10679 df-nn 11446 df-n0 11714 df-z 11800 df-uz 12065 df-fz 12715 df-fzo 12856 df-hash 13512 df-word 13679 df-concat 13740 df-s1 13765 df-s2 14078 df-s3 14079 df-s4 14080 df-vtx 26501 df-iedg 26502 |
This theorem is referenced by: usgrexmplvtx 26761 usgrexmpledg 26762 usgrexmpl 26763 |
Copyright terms: Public domain | W3C validator |