![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > fusgreg2wsplem | Structured version Visualization version GIF version |
Description: Lemma for fusgreg2wsp 29280 and related theorems. (Contributed by AV, 8-Jan-2022.) |
Ref | Expression |
---|---|
frgrhash2wsp.v | ⢠ð = (Vtxâðº) |
fusgreg2wsp.m | ⢠ð = (ð â ð ⊠{ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð}) |
Ref | Expression |
---|---|
fusgreg2wsplem | ⢠(ð â ð â (ð â (ðâð) â (ð â (2 WSPathsN ðº) ⧠(ðâ1) = ð))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eqeq2 2748 | . . . . 5 ⢠(ð = ð â ((ð€â1) = ð â (ð€â1) = ð)) | |
2 | 1 | rabbidv 3415 | . . . 4 ⢠(ð = ð â {ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð} = {ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð}) |
3 | fusgreg2wsp.m | . . . 4 ⢠ð = (ð â ð ⊠{ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð}) | |
4 | ovex 7390 | . . . . 5 ⢠(2 WSPathsN ðº) â V | |
5 | 4 | rabex 5289 | . . . 4 ⢠{ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð} â V |
6 | 2, 3, 5 | fvmpt 6948 | . . 3 ⢠(ð â ð â (ðâð) = {ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð}) |
7 | 6 | eleq2d 2823 | . 2 ⢠(ð â ð â (ð â (ðâð) â ð â {ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð})) |
8 | fveq1 6841 | . . . 4 ⢠(ð€ = ð â (ð€â1) = (ðâ1)) | |
9 | 8 | eqeq1d 2738 | . . 3 ⢠(ð€ = ð â ((ð€â1) = ð â (ðâ1) = ð)) |
10 | 9 | elrab 3645 | . 2 ⢠(ð â {ð€ â (2 WSPathsN ðº) ⣠(ð€â1) = ð} â (ð â (2 WSPathsN ðº) ⧠(ðâ1) = ð)) |
11 | 7, 10 | bitrdi 286 | 1 ⢠(ð â ð â (ð â (ðâð) â (ð â (2 WSPathsN ðº) ⧠(ðâ1) = ð))) |
Colors of variables: wff setvar class |
Syntax hints: â wi 4 â wb 205 ⧠wa 396 = wceq 1541 â wcel 2106 {crab 3407 ⊠cmpt 5188 âcfv 6496 (class class class)co 7357 1c1 11052 2c2 12208 Vtxcvtx 27947 WSPathsN cwwspthsn 28773 |
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 1913 ax-6 1971 ax-7 2011 ax-8 2108 ax-9 2116 ax-10 2137 ax-11 2154 ax-12 2171 ax-ext 2707 ax-sep 5256 ax-nul 5263 ax-pr 5384 |
This theorem depends on definitions: df-bi 206 df-an 397 df-or 846 df-3an 1089 df-tru 1544 df-fal 1554 df-ex 1782 df-nf 1786 df-sb 2068 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2889 df-ne 2944 df-ral 3065 df-rex 3074 df-rab 3408 df-v 3447 df-dif 3913 df-un 3915 df-in 3917 df-ss 3927 df-nul 4283 df-if 4487 df-sn 4587 df-pr 4589 df-op 4593 df-uni 4866 df-br 5106 df-opab 5168 df-mpt 5189 df-id 5531 df-xp 5639 df-rel 5640 df-cnv 5641 df-co 5642 df-dm 5643 df-iota 6448 df-fun 6498 df-fv 6504 df-ov 7360 |
This theorem is referenced by: fusgr2wsp2nb 29278 fusgreg2wsp 29280 2wspmdisj 29281 |
Copyright terms: Public domain | W3C validator |